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

Theorem anim2i 324
Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
anim1i.1
Assertion
Ref Expression
anim2i

Proof of Theorem anim2i
StepHypRef Expression
1 id 19 . 2
2 anim1i.1 . 2
31, 2anim12i 321 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 is referenced by:  sylanl2  383  sylanr2  385  andi  730  pm4.55dc  845  xoranor  1267  19.41h  1572  sbimi  1644  equs5e  1673  exdistrfor  1678  equs45f  1680  sbidm  1728  eu3h  1942  eupickb  1978  2exeu  1989  darii  1997  festino  2003  baroco  2004  r19.27av  2442  rspc2ev  2658  reu3  2725  sspssn  3042  difdif  3063  ssddif  3165  inssdif  3167  difin  3168  difindiss  3185  indifdir  3187  difrab  3205  iundif2ss  3713  trssord  4083  ordsuc  4241  find  4265  imainss  4682  dffun5r  4857  fof  5049  f1ocnv  5082  fv3  5140  relelfvdm  5148  funimass4  5167  fvelimab  5172  funconstss  5228  dff2  5254  dffo5  5259  dff1o6  5359  oprabid  5480  ssoprab2i  5535  releldm2  5753  recexgt0sr  6681  lediv2a  7622  elfzp12  8711
  Copyright terms: Public domain W3C validator