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  882  xoranor  1311  19.41h  1618  sbimi  1691  equs5e  1720  exdistrfor  1725  equs45f  1727  sbidm  1776  eu3h  1990  eupickb  2026  2exeu  2037  darii  2045  festino  2051  baroco  2052  r19.27av  2500  rspc2ev  2728  reu3  2796  difdif  3114  ssddif  3222  inssdif  3224  difin  3225  difindiss  3242  indifdir  3244  difrab  3262  iundif2ss  3778  trssord  4180  ordsuc  4351  find  4386  imainss  4810  dffun5r  4990  fof  5190  f1ocnv  5223  fv3  5285  relelfvdm  5293  funimass4  5312  fvelimab  5317  funconstss  5374  dff2  5400  dffo5  5405  dff1o6  5510  oprabid  5632  ssoprab2i  5688  releldm2  5906  recexgt0sr  7256  lediv2a  8284  lbreu  8334  elfzp12  9436  focdmex  10084  fihashf1rn  10086  cau3lem  10435  dvdsnegb  10680  dvds2add  10697  dvds2sub  10698  ndvdssub  10797  gcd2n0cl  10828  divgcdcoprmex  10951  cncongr1  10952
  Copyright terms: Public domain W3C validator