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

Theorem 3anim3i 1185
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 1182 1  |-  ( ( ch  /\  th  /\  ph )  ->  ( ch  /\ 
th  /\  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 974
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 976
This theorem is referenced by:  syl3anl3  1279  syl3anr3  1283  elioo4g  11596  ssnn0fi  12076  tmdcn2  20566  axcont  24257  constr3lem4  24625  extwwlkfab  25068  minvecolem3  25770  btwnconn1lem4  29716  btwnconn1lem5  29717  btwnconn1lem6  29718  bnj556  33826  bnj557  33827  bnj1145  33917  bj-ceqsalt  34334  bj-ceqsaltv  34335
  Copyright terms: Public domain W3C validator