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

Theorem 3anim3i 1175
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 22 . 2  |-  ( ch 
->  ch )
2 id 22 . 2  |-  ( th 
->  th )
3 3animi.1 . 2  |-  ( ph  ->  ps )
41, 2, 33anim123i 1173 1  |-  ( ( ch  /\  th  /\  ph )  ->  ( ch  /\ 
th  /\  ps )
)
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:  syl3anl3  1268  syl3anr3  1272  elioo4g  11354  tmdcn2  19658  axcont  23220  constr3lem4  23531  minvecolem3  24275  btwnconn1lem4  28119  btwnconn1lem5  28120  btwnconn1lem6  28121  extwwlkfab  30680  ssnn0fi  30743  bnj556  31890  bnj557  31891  bnj1145  31981  bj-ceqsalt  32383  bj-ceqsaltv  32384
  Copyright terms: Public domain W3C validator