Theorem 3adantl3 1165

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)

Hypothesis

Ref	Expression
3adantl.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adantl3	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3adantl3

Step	Hyp	Ref	Expression
1		3simpa 1145	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜏) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 583	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  dif1en  8735  infpssrlem4  9717  fin23lem11  9728  tskwun  10195  gruf  10222  lediv2a  11523  prunioo  12859  nn0p1elfzo  13075  hashunsnggt  13751  rpnnen2lem7  15565  muldvds1  15626  muldvds2  15627  dvdscmul  15628  dvdsmulc  15629  rpexp  16054  pospropd  17736  mdetmul  21228  elcls  21678  iscnp4  21868  cnpnei  21869  cnpflf2  22605  cnpflf  22606  cnpfcf  22646  xbln0  23021  blcls  23113  iimulcl  23542  icccvx  23555  iscau2  23881  rrxcph  23996  cncombf  24262  mumul  25766  ax5seglem1  26722  ax5seglem2  26723  wwlksnext  27679  clwwlkinwwlk  27825  nvmul0or  28433  fh1  29401  fh2  29402  cm2j  29403  pjoi0  29500  hoadddi  29586  hmopco  29806  padct  30481  iocinif  30530  volfiniune  31599  eulerpartlemb  31736  ivthALT  33796  lindsadd  35050  cnambfre  35105  rngohomco  35412  rngoisoco  35420  pexmidlem3N  37268  hdmapglem7  39225  factwoffsmonot  39388  relexpmulg  40411  supxrgere  41965  supxrgelem  41969  supxrge  41970  infxr  41999  infleinflem2  42003  rexabslelem  42055  lptre2pt  42282  fnlimfvre  42316  limsupmnfuzlem  42368  climisp  42388  limsupgtlem  42419  dvnprodlem1  42588  ibliccsinexp  42593  iblioosinexp  42595  fourierdlem12  42761  fourierdlem41  42790  fourierdlem42  42791  fourierdlem48  42796  fourierdlem49  42797  fourierdlem51  42799  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem97  42845  etransclem24  42900  ioorrnopnlem  42946  issalnnd  42985  sge0rpcpnf  43060  sge0seq  43085  meaiuninc3v  43123  smfmullem4  43426  smflimsupmpt  43460  smfliminfmpt  43463  lincdifsn  44833