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

Theorem 3anim1i 1141
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 21 . 2  |-  ( ch 
->  ch )
3 id 21 . 2  |-  ( th 
->  th )
41, 2, 33anim123i 1140 1  |-  ( (
ph  /\  ch  /\  th )  ->  ( ps  /\  ch  /\  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  syl3an1  1218  syl3anl1  1233  syl3anr1  1237  elfiun  7437  elioc2  10975  elico2  10976  elicc2  10977  trliswlk  21541  isspthonpth  21586  cm2j  23124  btwnconn1lem4  26026  mzpcong  27039  dvdsleabs2  27057  usg2wotspth  28404  bnj544  29327  dalem53  30584  dalem54  30585  paddasslem14  30692
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator