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  1738  sbidm  1779  disamis  2059  fun11uni  5070  fabexg  5182  fores  5226  f1oabexg  5249  fun11iun  5258  fvelrnb  5336  ssimaex  5349  foeqcnvco  5551  f1eqcocnv  5552  isoini  5579  brtposg  6001  tfrcllemssrecs  6099  djuex  6715  elni2  6852  dmaddpqlem  6915  nqpi  6916  ltexnqq  6946  nq0nn  6980  nqnq0a  6992  nqnq0m  6993  elnp1st2nd  7014  mullocprlem  7108  cnegexlem3  7638  divmulasscomap  8137  lediv2a  8328  btwnz  8835  eluz2b2  9059  uz2mulcl  9064  eqreznegel  9068  elioo4g  9321  fz0fzelfz0  9503  fz0fzdiffz0  9506  2ffzeq  9517  elfzodifsumelfzo  9577  elfzom1elp1fzo  9578  zpnn0elfzo  9583  ioo0  9636  zmodidfzoimp  9726  expcl2lemap  9932  mulreap  10263  redivap  10273  imdivap  10280  caucvgrelemcau  10378  negdvdsb  10905  muldvds1  10914  muldvds2  10915  dvdsdivcl  10944  nn0ehalf  10996  nn0oddm1d2  11002  nnoddm1d2  11003  infssuzex  11038  divgcdnn  11059  coprmgcdb  11163  divgcdcoprm0  11176  pw2dvdslemn  11236
  Copyright terms: Public domain W3C validator