Theorem adantl3r 763

Description: Deduction adding 1 conjunct to antecedent. (Contributed by Alan Sare, 17-Oct-2017.)

Hypothesis

Ref	Expression
adantl3r.1	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
adantl3r	⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem adantl3r

Step	Hyp	Ref	Expression
1		id 23	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2	1	adantlr 728	. 2 ⊢ (((𝜑 ∧ 𝜂) ∧ 𝜓) → (𝜑 ∧ 𝜓))
3		adantl3r.1	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylanl1 693	1 ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  adantl4r  768  ad5ant134  1392  ad5ant135  1394  iscgrglt  28992  legov  29063  dfcgra2  29353  suppovss  33331  cyc3genpm  33769  elrgspnlem4  33862  rhmimaidl  34038  fedgmul  34319  zarclsun  34558  omssubadd  34988  circlemeth  35325  poimirlem29  38710  adantlllr  46198  supxrge  46492  xrralrecnnle  46536  rexabslelem  46570  limclner  46803  xlimmnfvlem2  46985  xlimmnfv  46986  xlimpnfvlem2  46989  xlimpnfv  46990  climxlim2lem  46997  icccncfext  47039  fourierdlem64  47322  fourierdlem73  47331  etransclem35  47421  sge0tsms  47532  hoicvr  47700  hspmbllem2  47779  smflimlem2  47924  smflimlem4  47926