MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anim1i Structured version   Unicode version

Theorem 3anim1i 1191
Description: Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)
Hypothesis
Ref Expression
3animi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
3anim1i  |-  ( (
ph  /\  ch  /\  th )  ->  ( ps  /\  ch  /\  th ) )

Proof of Theorem 3anim1i
StepHypRef Expression
1 3animi.1 . 2  |-  ( ph  ->  ps )
2 id 23 . 2  |-  ( ch 
->  ch )
3 id 23 . 2  |-  ( th 
->  th )
41, 2, 33anim123i 1190 1  |-  ( (
ph  /\  ch  /\  th )  ->  ( ps  /\  ch  /\  th ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984
This theorem is referenced by:  syl3an1  1297  syl3anl1  1312  syl3anr1  1316  fnsuppres  6944  elfiun  7941  elioc2  11686  elico2  11687  elicc2  11688  trliswlk  25140  isspthonpth  25185  usg2wotspth  25483  cm2j  27134  bnj544  29519  btwnconn1lem4  30668  relowlssretop  31526  dalem53  33028  dalem54  33029  paddasslem14  33136  mzpcong  35561  dvdsleabs2  35577
  Copyright terms: Public domain W3C validator