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

Theorem anim1i 327
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 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:  sylanl1  388  sylanr1  390  mpan10  451  sbcof2  1705  sbidm  1745  disamis  2025  fun11uni  4994  fabexg  5102  fores  5140  f1oabexg  5163  fun11iun  5172  fvelrnb  5246  ssimaex  5259  foeqcnvco  5455  f1eqcocnv  5456  isoini  5482  brtposg  5897  elni2  6440  dmaddpqlem  6503  nqpi  6504  ltexnqq  6534  nq0nn  6568  nqnq0a  6580  nqnq0m  6581  elnp1st2nd  6602  mullocprlem  6696  cnegexlem3  7221  lediv2a  7906  btwnz  8386  eluz2b2  8607  uz2mulcl  8612  eqreznegel  8616  elioo4g  8874  fz0fzelfz0  9056  fz0fzdiffz0  9059  2ffzeq  9070  elfzodifsumelfzo  9129  elfzom1elp1fzo  9130  zpnn0elfzo  9135  zmodidfzoimp  9269  expcl2lemap  9397  mulreap  9656  redivap  9666  imdivap  9673  caucvgrelemcau  9771  negdvdsb  10087  muldvds1  10095  muldvds2  10096  dvdsdivcl  10125  nn0ehalf  10178  nn0oddm1d2  10184  nnoddm1d2  10185  pw2dvdslemn  10196
  Copyright terms: Public domain W3C validator