Theorem adantl3r 749

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  adantl4r  754  iscgrglt  27765  legov  27836  dfcgra2  28081  suppovss  31906  cyc3genpm  32311  rhmimaidl  32550  fedgmul  32716  zarclsun  32850  omssubadd  33299  circlemeth  33652  poimirlem29  36517  adantlllr  43723  supxrge  44048  xrralrecnnle  44093  rexabslelem  44128  limclner  44367  xlimmnfvlem2  44549  xlimmnfv  44550  xlimpnfvlem2  44553  xlimpnfv  44554  climxlim2lem  44561  icccncfext  44603  fourierdlem64  44886  fourierdlem73  44895  etransclem35  44985  sge0tsms  45096  hoicvr  45264  hspmbllem2  45343  smflimlem2  45488  smflimlem4  45490