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  28459  legov  28530  dfcgra2  28775  suppovss  32624  cyc3genpm  33095  elrgspnlem4  33186  rhmimaidl  33370  fedgmul  33604  zarclsun  33843  omssubadd  34274  circlemeth  34614  poimirlem29  37639  adantlllr  45027  supxrge  45328  xrralrecnnle  45372  rexabslelem  45407  limclner  45642  xlimmnfvlem2  45824  xlimmnfv  45825  xlimpnfvlem2  45828  xlimpnfv  45829  climxlim2lem  45836  icccncfext  45878  fourierdlem64  46161  fourierdlem73  46170  etransclem35  46260  sge0tsms  46371  hoicvr  46539  hspmbllem2  46618  smflimlem2  46763  smflimlem4  46765