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

Theorem anim1i 327
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 325 1  |-  ( (
ph  /\  ch )  ->  ( ps  /\  ch ) )
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  1707  sbidm  1747  disamis  2027  fun11uni  4997  fabexg  5105  fores  5143  f1oabexg  5166  fun11iun  5175  fvelrnb  5249  ssimaex  5262  foeqcnvco  5458  f1eqcocnv  5459  isoini  5485  brtposg  5900  elni2  6470  dmaddpqlem  6533  nqpi  6534  ltexnqq  6564  nq0nn  6598  nqnq0a  6610  nqnq0m  6611  elnp1st2nd  6632  mullocprlem  6726  cnegexlem3  7251  lediv2a  7936  btwnz  8416  eluz2b2  8637  uz2mulcl  8642  eqreznegel  8646  elioo4g  8904  fz0fzelfz0  9086  fz0fzdiffz0  9089  2ffzeq  9100  elfzodifsumelfzo  9159  elfzom1elp1fzo  9160  zpnn0elfzo  9165  ioo0  9216  zmodidfzoimp  9304  expcl2lemap  9432  mulreap  9692  redivap  9702  imdivap  9709  caucvgrelemcau  9807  negdvdsb  10124  muldvds1  10132  muldvds2  10133  dvdsdivcl  10162  nn0ehalf  10215  nn0oddm1d2  10221  nnoddm1d2  10222  pw2dvdslemn  10253
  Copyright terms: Public domain W3C validator