Theorem adantl3r 748

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

Syntax hints:   → wi 4   ∧ wa 396

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

This theorem is referenced by:  adantl4r  753  iscgrglt  27285  legov  27356  dfcgra2  27601  suppovss  31425  cyc3genpm  31827  rhmimaidl  32028  fedgmul  32146  zarclsun  32263  omssubadd  32712  circlemeth  33065  poimirlem29  36045  adantlllr  43155  supxrge  43477  xrralrecnnle  43522  rexabslelem  43558  limclner  43793  xlimmnfvlem2  43975  xlimmnfv  43976  xlimpnfvlem2  43979  xlimpnfv  43980  climxlim2lem  43987  icccncfext  44029  fourierdlem64  44312  fourierdlem73  44321  etransclem35  44411  sge0tsms  44522  hoicvr  44690  hspmbllem2  44769  smflimlem2  44914  smflimlem4  44916