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

Theorem 3anim3i 1141
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 20 . 2  |-  ( ch 
->  ch )
2 id 20 . 2  |-  ( th 
->  th )
3 3animi.1 . 2  |-  ( ph  ->  ps )
41, 2, 33anim123i 1139 1  |-  ( ( ch  /\  th  /\  ph )  ->  ( ch  /\ 
th  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  syl3anl3  1234  syl3anr3  1238  elioo4g  10971  tmdcn2  18119  constr3lem4  21634  minvecolem3  22378  axcont  25915  btwnconn1lem4  26024  btwnconn1lem5  26025  btwnconn1lem6  26026  bnj556  29271  bnj557  29272  bnj1145  29362
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator