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

Theorem 3adantl2 1114
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
Hypothesis
Ref Expression
3adantl.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
3adantl2  |-  ( ( ( ph  /\  ta  /\ 
ps )  /\  ch )  ->  th )

Proof of Theorem 3adantl2
StepHypRef Expression
1 3simpb 955 . 2  |-  ( (
ph  /\  ta  /\  ps )  ->  ( ph  /\  ps ) )
2 3adantl.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 458 1  |-  ( ( ( ph  /\  ta  /\ 
ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3ad2antl1  1119  omord2  6777  nnmord  6842  axcc3  8282  lediv2a  9868  zdiv  10304  clatleglb  14516  mulgnn0subcl  14866  mulgsubcl  14867  ghmmulg  14981  obs2ss  16919  neiint  17131  cnpnei  17290  caublcls  19222  ipval2lem2  22161  ipval2lem5  22167  fh1  23081  cm2j  23083  hoadddi  23267  hoadddir  23268  axlowdimlem16  25808  stoweidlem44  27668  lautco  30591
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator