Theorem adantl3r 751

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 716	. 2 ⊢ (((𝜑 ∧ 𝜂) ∧ 𝜓) → (𝜑 ∧ 𝜓))
3		adantl3r.1	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylanl1 681	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  756  iscgrglt  28602  legov  28673  dfcgra2  28918  suppovss  32775  cyc3genpm  33250  elrgspnlem4  33343  rhmimaidl  33529  fedgmul  33813  zarclsun  34052  omssubadd  34482  circlemeth  34822  poimirlem29  37904  adantlllr  45403  supxrge  45701  xrralrecnnle  45745  rexabslelem  45780  limclner  46013  xlimmnfvlem2  46195  xlimmnfv  46196  xlimpnfvlem2  46199  xlimpnfv  46200  climxlim2lem  46207  icccncfext  46249  fourierdlem64  46532  fourierdlem73  46541  etransclem35  46631  sge0tsms  46742  hoicvr  46910  hspmbllem2  46989  smflimlem2  47134  smflimlem4  47136