ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anim2d Structured version   Unicode version

Theorem anim2d 320
Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
anim1d.1
Assertion
Ref Expression
anim2d

Proof of Theorem anim2d
StepHypRef Expression
1 idd 21 . 2
2 anim1d.1 . 2
31, 2anim12d 318 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  spsbim  1721  ssel  2933  sscon  3071  uniss  3592  trel3  3853  copsexg  3972  ssopab2  4003  coss1  4434  fununi  4910  imadif  4922  fss  4997  ssimaex  5177  opabbrex  5491  ssoprab2  5503  poxp  5794  xpdom2  6241
  Copyright terms: Public domain W3C validator