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

Theorem 3adantl3 1116
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 955 . 2  |-  ( (
ph  /\  ps  /\  ta )  ->  ( ph  /\  ps ) )
2 3adantl.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 459 1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  dif1enOLD  7341  dif1en  7342  infpssrlem4  8187  fin23lem11  8198  tskwun  8660  gruf  8687  lediv2a  9905  prunioo  11026  rpnnen2lem7  12821  muldvds1  12875  muldvds2  12876  dvdscmul  12877  dvdsmulc  12878  rpexp  13121  pospropd  14562  elcls  17138  iscnp4  17328  cnpnei  17329  cnpflf2  18033  cnpflf  18034  cnpfcf  18074  xbln0  18445  blcls  18537  iimulcl  18963  icccvx  18976  iscau2  19231  cncombf  19551  mumul  20965  nvmul0or  22134  fh1  23121  fh2  23122  cm2j  23123  pjoi0  23220  hoadddi  23307  hmopco  23527  iocinif  24145  volfiniune  24587  ax5seglem1  25868  ax5seglem2  25869  cnambfre  26256  ivthALT  26339  rngohomco  26591  rngoisoco  26599  ibliccsinexp  27722  iblioosinexp  27724  2cshw2lem3  28255  pexmidlem3N  30770  hdmapglem7  32731
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator