Theorem adantl3r 762

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  adantl4r  767  ad5ant134  1390  ad5ant135  1392  iscgrglt  28749  legov  28820  dfcgra2  29098  suppovss  32967  cyc3genpm  33413  elrgspnlem4  33506  rhmimaidl  33684  fedgmul  33966  zarclsun  34205  omssubadd  34635  circlemeth  34972  poimirlem29  38222  adantlllr  45685  supxrge  45980  xrralrecnnle  46024  rexabslelem  46058  limclner  46291  xlimmnfvlem2  46473  xlimmnfv  46474  xlimpnfvlem2  46477  xlimpnfv  46478  climxlim2lem  46485  icccncfext  46527  fourierdlem64  46810  fourierdlem73  46819  etransclem35  46909  sge0tsms  47020  hoicvr  47188  hspmbllem2  47267  smflimlem2  47412  smflimlem4  47414