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

Theorem anim2i 328
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 325 1 ((𝜒𝜑) → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  sylanl2  389  sylanr2  391  andi  742  pm4.55dc  857  xoranor  1284  19.41h  1591  sbimi  1663  equs5e  1692  exdistrfor  1697  equs45f  1699  sbidm  1747  eu3h  1961  eupickb  1997  2exeu  2008  darii  2016  festino  2022  baroco  2023  r19.27av  2465  rspc2ev  2686  reu3  2753  sspssn  3075  difdif  3096  ssddif  3198  inssdif  3200  difin  3201  difindiss  3218  indifdir  3220  difrab  3238  iundif2ss  3749  trssord  4144  ordsuc  4314  find  4349  imainss  4766  dffun5r  4941  fof  5133  f1ocnv  5166  fv3  5224  relelfvdm  5232  funimass4  5251  fvelimab  5256  funconstss  5312  dff2  5338  dffo5  5343  dff1o6  5443  oprabid  5564  ssoprab2i  5620  releldm2  5838  recexgt0sr  6915  lediv2a  7935  elfzp12  9062  cau3lem  9940  dvdsnegb  10124  dvds2add  10140  dvds2sub  10141
  Copyright terms: Public domain W3C validator