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

Theorem anim1i 338
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 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:  sylanl1  399  sylanr1  401  mpan10  465  sbcof2  1766  sbidm  1807  disamis  2088  r19.28v  2537  fun11uni  5163  fabexg  5280  fores  5324  f1oabexg  5347  fun11iun  5356  fvelrnb  5437  ssimaex  5450  foeqcnvco  5659  f1eqcocnv  5660  isoini  5687  brtposg  6119  tfrcllemssrecs  6217  fiintim  6785  djuex  6896  elni2  7090  dmaddpqlem  7153  nqpi  7154  ltexnqq  7184  nq0nn  7218  nqnq0a  7230  nqnq0m  7231  elnp1st2nd  7252  mullocprlem  7346  cnegexlem3  7907  divmulasscomap  8424  lediv2a  8621  btwnz  9138  eluz2b2  9365  uz2mulcl  9370  eqreznegel  9374  elioo4g  9685  fz0fzelfz0  9872  fz0fzdiffz0  9875  2ffzeq  9886  elfzodifsumelfzo  9946  elfzom1elp1fzo  9947  zpnn0elfzo  9952  ioo0  10005  zmodidfzoimp  10095  expcl2lemap  10273  mulreap  10604  redivap  10614  imdivap  10621  caucvgrelemcau  10720  negdvdsb  11436  muldvds1  11445  muldvds2  11446  dvdsdivcl  11475  nn0ehalf  11527  nn0oddm1d2  11533  nnoddm1d2  11534  infssuzex  11569  divgcdnn  11590  coprmgcdb  11696  divgcdcoprm0  11709  pw2dvdslemn  11770
  Copyright terms: Public domain W3C validator