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

Theorem 3anim3i 1179
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 1176 1  |-  ( ( ch  /\  th  /\  ph )  ->  ( ch  /\ 
th  /\  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 968
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 970
This theorem is referenced by:  syl3anl3  1273  syl3anr3  1277  elioo4g  11574  ssnn0fi  12050  tmdcn2  20316  axcont  23948  constr3lem4  24309  extwwlkfab  24753  minvecolem3  25454  btwnconn1lem4  29303  btwnconn1lem5  29304  btwnconn1lem6  29305  bnj556  32912  bnj557  32913  bnj1145  33003  bj-ceqsalt  33407  bj-ceqsaltv  33408
  Copyright terms: Public domain W3C validator