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

Theorem 3anim3i 1182
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 1179 1  |-  ( ( ch  /\  th  /\  ph )  ->  ( ch  /\ 
th  /\  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  syl3anl3  1276  syl3anr3  1280  elioo4g  11506  ssnn0fi  11997  tmdcn2  20673  axcont  24400  constr3lem4  24768  extwwlkfab  25211  minvecolem3  25909  btwnconn1lem4  29893  btwnconn1lem5  29894  btwnconn1lem6  29895  bnj556  34305  bnj557  34306  bnj1145  34396  bj-ceqsalt  34798  bj-ceqsaltv  34799
  Copyright terms: Public domain W3C validator