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  385  sylanr2  387  andi  719  pm4.55dc  834  xoranor  1253  19.41h  1557  sbimi  1629  equs5e  1658  exdistrfor  1663  equs45f  1665  sbidm  1713  eu3h  1927  eupickb  1963  2exeu  1974  darii  1982  festino  1988  baroco  1989  r19.27av  2426  rspc2ev  2641  reu3  2708  sspssn  3025  difdif  3046  ssddif  3148  inssdif  3150  difin  3151  difindiss  3168  indifdir  3170  difrab  3188  iundif2ss  3696  trssord  4066  ordsuc  4225  find  4249  imainss  4666  fof  5031  f1ocnv  5064  fv3  5122  relelfvdm  5130  funimass4  5149  fvelimab  5154  funconstss  5210  dff2  5236  dffo5  5241  dff1o6  5341  oprabid  5461  ssoprab2i  5516  releldm2  5734  recexsrlem  6520
  Copyright terms: Public domain W3C validator