Theorem 3adantl3 1167

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  dif1enALT  9059  infpssrlem4  10071  fin23lem11  10082  tskwun  10549  gruf  10576  lediv2a  11878  prunioo  13222  nn0p1elfzo  13439  hashunsnggt  14118  rpnnen2lem7  15938  muldvds1  15999  muldvds2  16000  dvdscmul  16001  dvdsmulc  16002  rpexp  16436  pospropd  18054  mdetmul  21781  elcls  22233  iscnp4  22423  cnpnei  22424  cnpflf2  23160  cnpflf  23161  cnpfcf  23201  xbln0  23576  blcls  23671  iimulcl  24109  icccvx  24122  iscau2  24450  rrxcph  24565  cncombf  24831  mumul  26339  ax5seglem1  27305  ax5seglem2  27306  wwlksnext  28267  clwwlkinwwlk  28413  nvmul0or  29021  fh1  29989  fh2  29990  cm2j  29991  pjoi0  30088  hoadddi  30174  hmopco  30394  padct  31063  iocinif  31111  volfiniune  32207  eulerpartlemb  32344  noetalem1  33953  ivthALT  34533  lindsadd  35779  cnambfre  35834  rngohomco  36141  rngoisoco  36149  pexmidlem3N  37993  hdmapglem7  39950  sticksstones12a  40120  factwoffsmonot  40170  relexpmulg  41325  supxrgere  42879  supxrgelem  42883  supxrge  42884  infxr  42913  infleinflem2  42917  rexabslelem  42965  lptre2pt  43188  fnlimfvre  43222  limsupmnfuzlem  43274  climisp  43294  limsupgtlem  43325  dvnprodlem1  43494  ibliccsinexp  43499  iblioosinexp  43501  fourierdlem12  43667  fourierdlem41  43696  fourierdlem42  43697  fourierdlem48  43702  fourierdlem49  43703  fourierdlem51  43705  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem97  43751  etransclem24  43806  ioorrnopnlem  43852  issalnnd  43891  sge0rpcpnf  43966  sge0seq  43991  meaiuninc3v  44029  smfmullem4  44339  smflimsupmpt  44373  smfliminfmpt  44376  lincdifsn  45776