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

Theorem anim1i 336
Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
anim1i.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
anim1i  |-  ( (
ph  /\  ch )  ->  ( ps  /\  ch ) )

Proof of Theorem anim1i
StepHypRef Expression
1 anim1i.1 . 2  |-  ( ph  ->  ps )
2 id 19 . 2  |-  ( ch 
->  ch )
31, 2anim12i 334 1  |-  ( (
ph  /\  ch )  ->  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  sylanl1  397  sylanr1  399  mpan10  463  sbcof2  1762  sbidm  1803  disamis  2084  r19.28v  2532  fun11uni  5149  fabexg  5266  fores  5310  f1oabexg  5333  fun11iun  5342  fvelrnb  5421  ssimaex  5434  foeqcnvco  5643  f1eqcocnv  5644  isoini  5671  brtposg  6103  tfrcllemssrecs  6201  fiintim  6768  djuex  6878  elni2  7064  dmaddpqlem  7127  nqpi  7128  ltexnqq  7158  nq0nn  7192  nqnq0a  7204  nqnq0m  7205  elnp1st2nd  7226  mullocprlem  7320  cnegexlem3  7856  divmulasscomap  8363  lediv2a  8557  btwnz  9068  eluz2b2  9293  uz2mulcl  9298  eqreznegel  9302  elioo4g  9604  fz0fzelfz0  9791  fz0fzdiffz0  9794  2ffzeq  9805  elfzodifsumelfzo  9865  elfzom1elp1fzo  9866  zpnn0elfzo  9871  ioo0  9924  zmodidfzoimp  10014  expcl2lemap  10192  mulreap  10523  redivap  10533  imdivap  10540  caucvgrelemcau  10638  negdvdsb  11351  muldvds1  11360  muldvds2  11361  dvdsdivcl  11390  nn0ehalf  11442  nn0oddm1d2  11448  nnoddm1d2  11449  infssuzex  11484  divgcdnn  11505  coprmgcdb  11609  divgcdcoprm0  11622  pw2dvdslemn  11682
  Copyright terms: Public domain W3C validator