ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anim2i Structured version   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  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  3712  trssord  4082  ordsuc  4240  find  4264  imainss  4681  fof  5047  f1ocnv  5080  fv3  5138  relelfvdm  5146  funimass4  5165  fvelimab  5170  funconstss  5226  dff2  5252  dffo5  5257  dff1o6  5357  oprabid  5477  ssoprab2i  5532  releldm2  5750  recexgt0sr  6653  lediv2a  7593  elfzp12  8677
  Copyright terms: Public domain W3C validator