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  6581  nnmord  6646  axcc3  8080  lediv2a  9666  zdiv  10098  clatleglb  14246  mulgnn0subcl  14596  mulgsubcl  14597  ghmmulg  14711  obs2ss  16645  neiint  16857  cnpnei  17009  caublcls  18750  ipval2lem2  21293  ipval2lem5  21299  fh1  22213  cm2j  22215  hoadddi  22399  hoadddir  22400  axlowdimlem16  24657  cmprtr  25499  cmpltr2  25510  cmperltr  25512  infmrlbOLD  26525  lautco  30908
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