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  6739  nnmord  6804  axcc3  8244  lediv2a  9829  zdiv  10265  clatleglb  14473  mulgnn0subcl  14823  mulgsubcl  14824  ghmmulg  14938  obs2ss  16872  neiint  17084  cnpnei  17243  caublcls  19125  ipval2lem2  22041  ipval2lem5  22047  fh1  22961  cm2j  22963  hoadddi  23147  hoadddir  23148  axlowdimlem16  25603  stoweidlem44  27454  lautco  30262
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