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

Theorem 3anim1i 1138
Description: Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)
Hypothesis
Ref Expression
3animi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
3anim1i  |-  ( (
ph  /\  ch  /\  th )  ->  ( ps  /\  ch  /\  th ) )

Proof of Theorem 3anim1i
StepHypRef Expression
1 3animi.1 . 2  |-  ( ph  ->  ps )
2 id 19 . 2  |-  ( ch 
->  ch )
3 id 19 . 2  |-  ( th 
->  th )
41, 2, 33anim123i 1137 1  |-  ( (
ph  /\  ch  /\  th )  ->  ( ps  /\  ch  /\  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  syl3an1  1215  syl3anl1  1230  syl3anr1  1234  elfiun  7183  elioc2  10713  elico2  10714  elicc2  10715  cm2j  22199  probcun  23621  cndprobin  23637  btwnconn1lem4  24713  flfneih  25560  mzpcong  27059  dvdsleabs2  27077  stoweidlem60  27809  bnj544  28926  dalem53  29914  dalem54  29915  paddasslem14  30022
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator