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

Theorem 3anim1i 1182
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 22 . 2  |-  ( ch 
->  ch )
3 id 22 . 2  |-  ( th 
->  th )
41, 2, 33anim123i 1181 1  |-  ( (
ph  /\  ch  /\  th )  ->  ( ps  /\  ch  /\  th ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  syl3an1  1261  syl3anl1  1276  syl3anr1  1280  fnsuppres  6928  elfiun  7891  elioc2  11588  elico2  11589  elicc2  11590  trliswlk  24314  isspthonpth  24359  usg2wotspth  24657  cm2j  26311  btwnconn1lem4  29593  mzpcong  30741  dvdsleabs2  30757  mullimc  31385  mullimcf  31392  bnj544  33248  dalem53  34738  dalem54  34739  paddasslem14  34846
  Copyright terms: Public domain W3C validator