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  27803  legov  27874  dfcgra2  28119  suppovss  31944  cyc3genpm  32352  rhmimaidl  32595  fedgmul  32775  zarclsun  32919  omssubadd  33368  circlemeth  33721  poimirlem29  36603  adantlllr  43805  supxrge  44127  xrralrecnnle  44172  rexabslelem  44207  limclner  44446  xlimmnfvlem2  44628  xlimmnfv  44629  xlimpnfvlem2  44632  xlimpnfv  44633  climxlim2lem  44640  icccncfext  44682  fourierdlem64  44965  fourierdlem73  44974  etransclem35  45064  sge0tsms  45175  hoicvr  45343  hspmbllem2  45422  smflimlem2  45567  smflimlem4  45569