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

Theorem anim1i 338
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 336 1  |-  ( (
ph  /\  ch )  ->  ( ps  /\  ch ) )
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  8423  lediv2a  8617  btwnz  9128  eluz2b2  9353  uz2mulcl  9358  eqreznegel  9362  elioo4g  9672  fz0fzelfz0  9859  fz0fzdiffz0  9862  2ffzeq  9873  elfzodifsumelfzo  9933  elfzom1elp1fzo  9934  zpnn0elfzo  9939  ioo0  9992  zmodidfzoimp  10082  expcl2lemap  10260  mulreap  10591  redivap  10601  imdivap  10608  caucvgrelemcau  10707  negdvdsb  11421  muldvds1  11430  muldvds2  11431  dvdsdivcl  11460  nn0ehalf  11512  nn0oddm1d2  11518  nnoddm1d2  11519  infssuzex  11554  divgcdnn  11575  coprmgcdb  11681  divgcdcoprm0  11694  pw2dvdslemn  11754
  Copyright terms: Public domain W3C validator