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  6801  nnmord  6866  axcc3  8307  lediv2a  9893  zdiv  10329  clatleglb  14541  mulgnn0subcl  14891  mulgsubcl  14892  ghmmulg  15006  obs2ss  16944  neiint  17156  cnpnei  17316  caublcls  19249  ipval2lem2  22188  ipval2lem5  22194  fh1  23108  cm2j  23110  hoadddi  23294  hoadddir  23295  axlowdimlem16  25844  stoweidlem44  27707  lautco  30733
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