Theorem 3adantl3 1164

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 1144	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜏) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 582	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  dif1en  8751  infpssrlem4  9728  fin23lem11  9739  tskwun  10206  gruf  10233  lediv2a  11534  prunioo  12868  nn0p1elfzo  13081  hashunsnggt  13756  rpnnen2lem7  15573  muldvds1  15634  muldvds2  15635  dvdscmul  15636  dvdsmulc  15637  rpexp  16064  pospropd  17744  mdetmul  21232  elcls  21681  iscnp4  21871  cnpnei  21872  cnpflf2  22608  cnpflf  22609  cnpfcf  22649  xbln0  23024  blcls  23116  iimulcl  23541  icccvx  23554  iscau2  23880  rrxcph  23995  cncombf  24259  mumul  25758  ax5seglem1  26714  ax5seglem2  26715  wwlksnext  27671  clwwlkinwwlk  27818  nvmul0or  28427  fh1  29395  fh2  29396  cm2j  29397  pjoi0  29494  hoadddi  29580  hmopco  29800  padct  30455  iocinif  30504  volfiniune  31489  eulerpartlemb  31626  ivthALT  33683  lindsadd  34900  cnambfre  34955  rngohomco  35267  rngoisoco  35275  pexmidlem3N  37123  hdmapglem7  39080  factwoffsmonot  39118  relexpmulg  40075  supxrgere  41621  supxrgelem  41625  supxrge  41626  infxr  41655  infleinflem2  41659  rexabslelem  41712  lptre2pt  41941  fnlimfvre  41975  limsupmnfuzlem  42027  climisp  42047  limsupgtlem  42078  dvnprodlem1  42251  ibliccsinexp  42256  iblioosinexp  42258  fourierdlem12  42424  fourierdlem41  42453  fourierdlem42  42454  fourierdlem48  42459  fourierdlem49  42460  fourierdlem51  42462  fourierdlem73  42484  fourierdlem74  42485  fourierdlem75  42486  fourierdlem97  42508  etransclem24  42563  ioorrnopnlem  42609  issalnnd  42648  sge0rpcpnf  42723  sge0seq  42748  meaiuninc3v  42786  smfmullem4  43089  smflimsupmpt  43123  smfliminfmpt  43126  lincdifsn  44499