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

Theorem anim2i 334
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 331 1 ((𝜒𝜑) → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  sylanl2  395  sylanr2  397  andi  765  pm4.55dc  880  xoranor  1309  19.41h  1616  sbimi  1689  equs5e  1718  exdistrfor  1723  equs45f  1725  sbidm  1774  eu3h  1988  eupickb  2024  2exeu  2035  darii  2043  festino  2049  baroco  2050  r19.27av  2498  rspc2ev  2725  reu3  2793  difdif  3109  ssddif  3216  inssdif  3218  difin  3219  difindiss  3236  indifdir  3238  difrab  3256  iundif2ss  3769  trssord  4170  ordsuc  4341  find  4376  imainss  4800  dffun5r  4980  fof  5180  f1ocnv  5213  fv3  5272  relelfvdm  5280  funimass4  5299  fvelimab  5304  funconstss  5361  dff2  5387  dffo5  5392  dff1o6  5494  oprabid  5615  ssoprab2i  5671  releldm2  5889  recexgt0sr  7221  lediv2a  8249  lbreu  8299  elfzp12  9405  focdmex  10029  fihashf1rn  10031  cau3lem  10373  dvdsnegb  10592  dvds2add  10609  dvds2sub  10610  ndvdssub  10709  gcd2n0cl  10740  divgcdcoprmex  10863  cncongr1  10864
  Copyright terms: Public domain W3C validator