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

Theorem 3adantl2 1112
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 953 . 2  |-  ( (
ph  /\  ta  /\  ps )  ->  ( ph  /\  ps ) )
2 3adantl.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 457 1  |-  ( ( ( ph  /\  ta  /\ 
ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3ad2antl1  1117  omord2  6652  nnmord  6717  axcc3  8154  lediv2a  9740  zdiv  10174  clatleglb  14329  mulgnn0subcl  14679  mulgsubcl  14680  ghmmulg  14794  obs2ss  16735  neiint  16947  cnpnei  17099  caublcls  18838  ipval2lem2  21391  ipval2lem5  21397  fh1  22311  cm2j  22313  hoadddi  22497  hoadddir  22498  axlowdimlem16  25144  infmrlbOLD  25746  lautco  30355
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