Theorem 3adantl3 1154

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 993	. 2 |- ( ( ph /\ ps /\ ta ) -> ( ph /\ ps ) )
2		3adantl.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylan 471	1 |- ( ( ( ph /\ ps /\ ta ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 973

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 185  df-an 371  df-3an 975

This theorem is referenced by:  dif1enOLD  7764  dif1en  7765  infpssrlem4  8698  fin23lem11  8709  tskwun  9174  gruf  9201  lediv2a  10451  prunioo  11661  rpnnen2lem7  13832  muldvds1  13886  muldvds2  13887  dvdscmul  13888  dvdsmulc  13889  rpexp  14137  pospropd  15638  mdetmul  18994  elcls  19442  iscnp4  19632  cnpnei  19633  cnpflf2  20369  cnpflf  20370  cnpfcf  20410  xbln0  20785  blcls  20877  iimulcl  21305  icccvx  21318  iscau2  21584  rrxcph  21692  cncombf  21933  mumul  23321  f1otrg  23997  ax5seglem1  24054  ax5seglem2  24055  wwlkext2clwwlk  24626  nvmul0or  25370  fh1  26359  fh2  26360  cm2j  26361  pjoi0  26458  hoadddi  26545  hmopco  26765  iocinif  27415  volfiniune  28027  eulerpartlemb  28132  cnambfre  29990  ivthALT  30080  rngohomco  30304  rngoisoco  30312  lptre2pt  31505  ibliccsinexp  31591  iblioosinexp  31593  fourierdlem12  31742  fourierdlem41  31771  fourierdlem42  31772  fourierdlem48  31778  fourierdlem49  31779  fourierdlem51  31781  fourierdlem73  31803  fourierdlem74  31804  fourierdlem75  31805  fourierdlem97  31827  lincdifsn  32507  pexmidlem3N  35169  hdmapglem7  37130