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

Theorem 3adantl2 1151
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 992 . 2  |-  ( (
ph  /\  ta  /\  ps )  ->  ( ph  /\  ps ) )
2 3adantl.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 469 1  |-  ( ( ( ph  /\  ta  /\ 
ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973
This theorem is referenced by:  3ad2antl1  1156  omord2  7208  nnmord  7273  axcc3  8809  lediv2a  10434  zdiv  10929  clatleglb  15955  mulgnn0subcl  16354  mulgsubcl  16355  ghmmulg  16478  obs2ss  18933  scmatf1  19200  neiint  19772  cnpnei  19932  caublcls  21913  axlowdimlem16  24462  clwwlkext2edg  25004  ipval2lem2  25812  ipval2lem5  25818  fh1  26734  cm2j  26736  hoadddi  26920  hoadddir  26921  stoweidlem44  32065  fourierdlem41  32169  fourierdlem42  32170  fourierdlem54  32182  fourierdlem83  32211  lautco  36218
  Copyright terms: Public domain W3C validator