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

Theorem 3adantl3 1115
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
3adantl3  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )

Proof of Theorem 3adantl3
StepHypRef Expression
1 3simpa 954 . 2  |-  ( (
ph  /\  ps  /\  ta )  ->  ( ph  /\  ps ) )
2 3adantl.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 458 1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  dif1enOLD  7331  dif1en  7332  infpssrlem4  8175  fin23lem11  8186  tskwun  8648  gruf  8675  lediv2a  9893  prunioo  11014  rpnnen2lem7  12808  muldvds1  12862  muldvds2  12863  dvdscmul  12864  dvdsmulc  12865  rpexp  13108  pospropd  14549  elcls  17125  iscnp4  17315  cnpnei  17316  cnpflf2  18020  cnpflf  18021  cnpfcf  18061  xbln0  18432  blcls  18524  iimulcl  18950  icccvx  18963  iscau2  19218  cncombf  19538  mumul  20952  nvmul0or  22121  fh1  23108  fh2  23109  cm2j  23110  pjoi0  23207  hoadddi  23294  hmopco  23514  iocinif  24132  volfiniune  24574  ax5seglem1  25815  ax5seglem2  25816  cnambfre  26201  ivthALT  26275  rngohomco  26527  rngoisoco  26535  ibliccsinexp  27659  iblioosinexp  27661  2shwrd2lem3  28144  pexmidlem3N  30608  hdmapglem7  32569
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