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  7343  dif1en  7344  infpssrlem4  8191  fin23lem11  8202  tskwun  8664  gruf  8691  lediv2a  9909  prunioo  11030  rpnnen2lem7  12825  muldvds1  12879  muldvds2  12880  dvdscmul  12881  dvdsmulc  12882  rpexp  13125  pospropd  14566  elcls  17142  iscnp4  17332  cnpnei  17333  cnpflf2  18037  cnpflf  18038  cnpfcf  18078  xbln0  18449  blcls  18541  iimulcl  18967  icccvx  18980  iscau2  19235  cncombf  19553  mumul  20969  nvmul0or  22138  fh1  23125  fh2  23126  cm2j  23127  pjoi0  23224  hoadddi  23311  hmopco  23531  iocinif  24149  volfiniune  24591  ax5seglem1  25872  ax5seglem2  25873  cnambfre  26267  ivthALT  26352  rngohomco  26604  rngoisoco  26612  ibliccsinexp  27735  iblioosinexp  27737  2cshw2lem3  28288  pexmidlem3N  30843  hdmapglem7  32804
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator