Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  anim2i GIF 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  731  pm4.55dc  846  xoranor  1268  19.41h  1575  sbimi  1647  equs5e  1676  exdistrfor  1681  equs45f  1683  sbidm  1731  eu3h  1945  eupickb  1981  2exeu  1992  darii  2000  festino  2006  baroco  2007  r19.27av  2448  rspc2ev  2664  reu3  2731  sspssn  3048  difdif  3069  ssddif  3171  inssdif  3173  difin  3174  difindiss  3191  indifdir  3193  difrab  3211  iundif2ss  3722  trssord  4117  ordsuc  4287  find  4322  imainss  4739  dffun5r  4914  fof  5106  f1ocnv  5139  fv3  5197  relelfvdm  5205  funimass4  5224  fvelimab  5229  funconstss  5285  dff2  5311  dffo5  5316  dff1o6  5416  oprabid  5537  ssoprab2i  5593  releldm2  5811  recexgt0sr  6858  lediv2a  7861  elfzp12  8961  cau3lem  9710
 Copyright terms: Public domain W3C validator