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

Theorem 3anim1i 1174
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 1173 1  |-  ( (
ph  /\  ch  /\  th )  ->  ( ps  /\  ch  /\  th ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 967
This theorem is referenced by:  syl3an1  1251  syl3anl1  1266  syl3anr1  1270  fnsuppres  6716  elfiun  7680  elioc2  11358  elico2  11359  elicc2  11360  trliswlk  23438  isspthonpth  23483  cm2j  25023  btwnconn1lem4  28121  mzpcong  29315  dvdsleabs2  29333  usg2wotspth  30403  bnj544  31887  dalem53  33369  dalem54  33370  paddasslem14  33477
  Copyright terms: Public domain W3C validator