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

Theorem anim1i 333
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 331 1  |-  ( (
ph  /\  ch )  ->  ( ps  /\  ch ) )
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  5084  fabexg  5198  fores  5242  f1oabexg  5265  fun11iun  5274  fvelrnb  5352  ssimaex  5365  foeqcnvco  5569  f1eqcocnv  5570  isoini  5597  brtposg  6019  tfrcllemssrecs  6117  fiintim  6639  djuex  6736  elni2  6873  dmaddpqlem  6936  nqpi  6937  ltexnqq  6967  nq0nn  7001  nqnq0a  7013  nqnq0m  7014  elnp1st2nd  7035  mullocprlem  7129  cnegexlem3  7659  divmulasscomap  8163  lediv2a  8356  btwnz  8865  eluz2b2  9090  uz2mulcl  9095  eqreznegel  9099  elioo4g  9352  fz0fzelfz0  9538  fz0fzdiffz0  9541  2ffzeq  9552  elfzodifsumelfzo  9612  elfzom1elp1fzo  9613  zpnn0elfzo  9618  ioo0  9671  zmodidfzoimp  9761  expcl2lemap  9967  mulreap  10298  redivap  10308  imdivap  10315  caucvgrelemcau  10413  negdvdsb  11090  muldvds1  11099  muldvds2  11100  dvdsdivcl  11129  nn0ehalf  11181  nn0oddm1d2  11187  nnoddm1d2  11188  infssuzex  11223  divgcdnn  11244  coprmgcdb  11348  divgcdcoprm0  11361  pw2dvdslemn  11421
  Copyright terms: Public domain W3C validator