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

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

Proof of Theorem 3anim3i
StepHypRef Expression
1 id 19 . 2  |-  ( ch 
->  ch )
2 id 19 . 2  |-  ( th 
->  th )
3 3animi.1 . 2  |-  ( ph  ->  ps )
41, 2, 33anim123i 1137 1  |-  ( ( ch  /\  th  /\  ph )  ->  ( ch  /\ 
th  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  syl3anl3  1232  syl3anr3  1236  elioo4g  10727  tmdcn2  17788  minvecolem3  21471  axcont  24676  btwnconn1lem4  24785  btwnconn1lem5  24786  btwnconn1lem6  24787  posprsr  25343  constr3lem4  28393  bnj556  29248  bnj557  29249  bnj1145  29339
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator