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  26294  legov  26365  dfcgra2  26610  suppovss  30420  cyc3genpm  30789  fedgmul  31022  omssubadd  31553  circlemeth  31906  poimirlem29  34915  adantlllr  41290  supxrge  41599  xrralrecnnle  41646  rexabslelem  41685  limclner  41925  xlimmnfvlem2  42107  xlimmnfv  42108  xlimpnfvlem2  42111  xlimpnfv  42112  climxlim2lem  42119  icccncfext  42163  fourierdlem64  42449  fourierdlem73  42458  etransclem35  42548  sge0tsms  42656  hoicvr  42824  hspmbllem2  42903  smflimlem2  43042  smflimlem4  43044