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  9038  infpssrlem4  10073  fin23lem11  10084  tskwun  10551  gruf  10578  lediv2a  11880  prunioo  13224  nn0p1elfzo  13441  hashunsnggt  14120  rpnnen2lem7  15940  muldvds1  16001  muldvds2  16002  dvdscmul  16003  dvdsmulc  16004  rpexp  16438  pospropd  18056  mdetmul  21783  elcls  22235  iscnp4  22425  cnpnei  22426  cnpflf2  23162  cnpflf  23163  cnpfcf  23203  xbln0  23578  blcls  23673  iimulcl  24111  icccvx  24124  iscau2  24452  rrxcph  24567  cncombf  24833  mumul  26341  ax5seglem1  27307  ax5seglem2  27308  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  37995  hdmapglem7  39952  sticksstones12a  40122  factwoffsmonot  40172  relexpmulg  41300  supxrgere  42854  supxrgelem  42858  supxrge  42859  infxr  42888  infleinflem2  42892  rexabslelem  42940  lptre2pt  43163  fnlimfvre  43197  limsupmnfuzlem  43249  climisp  43269  limsupgtlem  43300  dvnprodlem1  43469  ibliccsinexp  43474  iblioosinexp  43476  fourierdlem12  43642  fourierdlem41  43671  fourierdlem42  43672  fourierdlem48  43677  fourierdlem49  43678  fourierdlem51  43680  fourierdlem73  43702  fourierdlem74  43703  fourierdlem75  43704  fourierdlem97  43726  etransclem24  43781  ioorrnopnlem  43827  issalnnd  43866  sge0rpcpnf  43941  sge0seq  43966  meaiuninc3v  44004  smfmullem4  44307  smflimsupmpt  44341  smfliminfmpt  44344  lincdifsn  45744