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 398

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 399

This theorem is referenced by:  adantl4r  753  iscgrglt  26300  legov  26371  dfcgra2  26616  suppovss  30426  cyc3genpm  30794  fedgmul  31027  omssubadd  31558  circlemeth  31911  poimirlem29  34936  adantlllr  41317  supxrge  41626  xrralrecnnle  41673  rexabslelem  41712  limclner  41952  xlimmnfvlem2  42134  xlimmnfv  42135  xlimpnfvlem2  42138  xlimpnfv  42139  climxlim2lem  42146  icccncfext  42190  fourierdlem64  42475  fourierdlem73  42484  etransclem35  42574  sge0tsms  42682  hoicvr  42850  hspmbllem2  42929  smflimlem2  43068  smflimlem4  43070