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

Theorem anim2i 340
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 336 1 ((𝜒𝜑) → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  sylanl2  401  sylanr2  403  andi  808  pm4.55dc  923  xoranor  1356  19.41h  1664  sbimi  1738  equs5e  1768  exdistrfor  1773  equs45f  1775  sbidm  1824  eu3h  2045  eupickb  2081  2exeu  2092  darii  2100  festino  2106  baroco  2107  r19.27v  2562  r19.27av  2570  rspc2ev  2807  reu3  2877  difdif  3205  ssddif  3314  inssdif  3316  difin  3317  difindiss  3334  indifdir  3336  difrab  3354  iundif2ss  3885  trssord  4309  ordsuc  4485  find  4520  imainss  4961  dffun5r  5142  fof  5352  f1ocnv  5387  fv3  5451  relelfvdm  5460  funimass4  5479  fvelimab  5484  funconstss  5545  dff2  5571  dffo5  5576  dff1o6  5684  oprabid  5810  ssoprab2i  5867  releldm2  6090  ixpf  6621  recexgt0sr  7604  map2psrprg  7636  lediv2a  8676  lbreu  8726  elfzp12  9909  focdmex  10564  fihashf1rn  10566  cau3lem  10917  fsumcl2lem  11198  dvdsnegb  11544  dvds2add  11561  dvds2sub  11562  ndvdssub  11661  gcd2n0cl  11692  divgcdcoprmex  11817  cncongr1  11818  ctinfom  11975  istopfin  12204  toponcom  12231  cnptoprest  12445
  Copyright terms: Public domain W3C validator