Theorem 3adantl3 1219

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

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  dif1en  8193  infpssrlem4  9128  fin23lem11  9139  tskwun  9606  gruf  9633  lediv2a  10917  prunioo  12301  nn0p1elfzo  12510  rpnnen2lem7  14949  muldvds1  15006  muldvds2  15007  dvdscmul  15008  dvdsmulc  15009  rpexp  15432  pospropd  17134  mdetmul  20429  elcls  20877  iscnp4  21067  cnpnei  21068  cnpflf2  21804  cnpflf  21805  cnpfcf  21845  xbln0  22219  blcls  22311  iimulcl  22736  icccvx  22749  iscau2  23075  rrxcph  23180  cncombf  23425  mumul  24907  ax5seglem1  25808  ax5seglem2  25809  clwwlkinwwlk  26905  wwlksext2clwwlk  26924  nvmul0or  27505  fh1  28477  fh2  28478  cm2j  28479  pjoi0  28576  hoadddi  28662  hmopco  28882  padct  29497  iocinif  29543  volfiniune  30293  eulerpartlemb  30430  ivthALT  32330  cnambfre  33458  rngohomco  33773  rngoisoco  33781  pexmidlem3N  35258  hdmapglem7  37221  relexpmulg  38002  supxrgere  39549  supxrgelem  39553  supxrge  39554  infxr  39583  infleinflem2  39587  rexabslelem  39645  lptre2pt  39872  fnlimfvre  39906  limsupmnfuzlem  39958  climisp  39978  limsupgtlem  40009  dvnprodlem1  40161  ibliccsinexp  40166  iblioosinexp  40168  fourierdlem12  40336  fourierdlem41  40365  fourierdlem42  40366  fourierdlem48  40371  fourierdlem49  40372  fourierdlem51  40374  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem97  40420  etransclem24  40475  ioorrnopnlem  40524  issalnnd  40563  sge0rpcpnf  40638  sge0seq  40663  smfmullem4  41001  smflimsupmpt  41035  smfliminfmpt  41038  lincdifsn  42213