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

Theorem anim1i 333
Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
anim1i.1 (𝜑𝜓)
Assertion
Ref Expression
anim1i ((𝜑𝜒) → (𝜓𝜒))

Proof of Theorem anim1i
StepHypRef Expression
1 anim1i.1 . 2 (𝜑𝜓)
2 id 19 . 2 (𝜒𝜒)
31, 2anim12i 331 1 ((𝜑𝜒) → (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  sylanl1  394  sylanr1  396  mpan10  458  sbcof2  1733  sbidm  1774  disamis  2054  fun11uni  5020  fabexg  5128  fores  5167  f1oabexg  5190  fun11iun  5199  fvelrnb  5274  ssimaex  5287  foeqcnvco  5482  f1eqcocnv  5483  isoini  5509  brtposg  5924  tfrcllemssrecs  6022  djuex  6553  elni2  6636  dmaddpqlem  6699  nqpi  6700  ltexnqq  6730  nq0nn  6764  nqnq0a  6776  nqnq0m  6777  elnp1st2nd  6798  mullocprlem  6892  cnegexlem3  7422  divmulasscomap  7921  lediv2a  8110  btwnz  8617  eluz2b2  8841  uz2mulcl  8846  eqreznegel  8850  elioo4g  9103  fz0fzelfz0  9285  fz0fzdiffz0  9288  2ffzeq  9298  elfzodifsumelfzo  9357  elfzom1elp1fzo  9358  zpnn0elfzo  9363  ioo0  9416  zmodidfzoimp  9506  expcl2lemap  9655  mulreap  9970  redivap  9980  imdivap  9987  caucvgrelemcau  10085  negdvdsb  10437  muldvds1  10446  muldvds2  10447  dvdsdivcl  10476  nn0ehalf  10528  nn0oddm1d2  10534  nnoddm1d2  10535  infssuzex  10570  divgcdnn  10591  coprmgcdb  10695  divgcdcoprm0  10708  pw2dvdslemn  10768
  Copyright terms: Public domain W3C validator