Theorem adantl3r 750

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  adantl4r  755  iscgrglt  28586  legov  28657  dfcgra2  28902  suppovss  32760  cyc3genpm  33234  elrgspnlem4  33327  rhmimaidl  33513  fedgmul  33788  zarclsun  34027  omssubadd  34457  circlemeth  34797  poimirlem29  37850  adantlllr  45294  supxrge  45593  xrralrecnnle  45637  rexabslelem  45672  limclner  45905  xlimmnfvlem2  46087  xlimmnfv  46088  xlimpnfvlem2  46091  xlimpnfv  46092  climxlim2lem  46099  icccncfext  46141  fourierdlem64  46424  fourierdlem73  46433  etransclem35  46523  sge0tsms  46634  hoicvr  46802  hspmbllem2  46881  smflimlem2  47026  smflimlem4  47028