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  7199  elioc2  10729  elico2  10730  elicc2  10731  cm2j  22215  probcun  23636  cndprobin  23652  btwnconn1lem4  24785  flfneih  25663  mzpcong  27162  dvdsleabs2  27180  stoweidlem60  27912  trliswlk  28338  bnj544  29242  dalem53  30536  dalem54  30537  paddasslem14  30644
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