Theorem adantl3r 760

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 22	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2	1	adantlr 725	. 2 ⊢ (((𝜑 ∧ 𝜂) ∧ 𝜓) → (𝜑 ∧ 𝜓))
3		adantl3r.1	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylanl1 690	1 ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  adantl4r  765  ad5ant134  1384  ad5ant135  1386  iscgrglt  28683  legov  28754  dfcgra2  29024  suppovss  32883  cyc3genpm  33332  elrgspnlem4  33426  rhmimaidl  33618  fedgmul  33928  zarclsun  34167  omssubadd  34597  circlemeth  34934  poimirlem29  38148  adantlllr  45619  supxrge  45914  xrralrecnnle  45958  rexabslelem  45992  limclner  46225  xlimmnfvlem2  46407  xlimmnfv  46408  xlimpnfvlem2  46411  xlimpnfv  46412  climxlim2lem  46419  icccncfext  46461  fourierdlem64  46744  fourierdlem73  46753  etransclem35  46843  sge0tsms  46954  hoicvr  47122  hspmbllem2  47201  smflimlem2  47346  smflimlem4  47348