Theorem 3adantl3 1163

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

Step	Hyp	Ref	Expression
1		3simpa 1002	. 2 |- ( ( ph /\ ps /\ ta ) -> ( ph /\ ps ) )
2		3adantl.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylan 473	1 |- ( ( ( ph /\ ps /\ ta ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  dif1en  7801  infpssrlem4  8725  fin23lem11  8736  tskwun  9198  gruf  9225  lediv2a  10489  prunioo  11748  rpnnen2lem7  14240  muldvds1  14294  muldvds2  14295  dvdscmul  14296  dvdsmulc  14297  rpexp  14632  pospropd  16332  mdetmul  19585  elcls  20026  iscnp4  20216  cnpnei  20217  cnpflf2  20952  cnpflf  20953  cnpfcf  20993  xbln0  21366  blcls  21458  iimulcl  21887  icccvx  21900  iscau2  22166  rrxcph  22270  cncombf  22521  mumul  24010  ax5seglem1  24845  ax5seglem2  24846  wwlkext2clwwlk  25417  nvmul0or  26159  fh1  27147  fh2  27148  cm2j  27149  pjoi0  27246  hoadddi  27332  hmopco  27552  padct  28191  iocinif  28240  volfiniune  28933  eulerpartlemb  29068  ivthALT  30817  cnambfre  31737  rngohomco  31961  rngoisoco  31969  pexmidlem3N  33290  hdmapglem7  35253  relexpmulg  35989  supxrgere  37213  supxrgelem  37217  supxrge  37218  lptre2pt  37340  dvnprodlem1  37438  ibliccsinexp  37444  iblioosinexp  37446  fourierdlem12  37598  fourierdlem41  37627  fourierdlem42  37628  fourierdlem48  37634  fourierdlem49  37635  fourierdlem51  37637  fourierdlem73  37659  fourierdlem74  37660  fourierdlem75  37661  fourierdlem97  37683  etransclem24  37738  lincdifsn  39034