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

Theorem 3adantl2 1145
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 986 . 2  |-  ( (
ph  /\  ta  /\  ps )  ->  ( ph  /\  ps ) )
2 3adantl.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 471 1  |-  ( ( ( ph  /\  ta  /\ 
ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 371  df-3an 967
This theorem is referenced by:  3ad2antl1  1150  omord2  7119  nnmord  7184  axcc3  8721  lediv2a  10340  zdiv  10826  clatleglb  15418  mulgnn0subcl  15762  mulgsubcl  15763  ghmmulg  15881  obs2ss  18282  neiint  18843  cnpnei  19003  caublcls  20954  axlowdimlem16  23375  ipval2lem2  24271  ipval2lem5  24277  fh1  25193  cm2j  25195  hoadddi  25379  hoadddir  25380  stoweidlem44  30007  lautco  34099
  Copyright terms: Public domain W3C validator