Theorem adantl3r 746

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 711	. 2 ⊢ (((𝜑 ∧ 𝜂) ∧ 𝜓) → (𝜑 ∧ 𝜓))
3		adantl3r.1	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylanl1 676	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 206  df-an 396

This theorem is referenced by:  adantl4r  751  iscgrglt  26779  legov  26850  dfcgra2  27095  suppovss  30919  cyc3genpm  31321  rhmimaidl  31511  fedgmul  31614  zarclsun  31722  omssubadd  32167  circlemeth  32520  poimirlem29  35733  adantlllr  42472  supxrge  42767  xrralrecnnle  42812  rexabslelem  42848  limclner  43082  xlimmnfvlem2  43264  xlimmnfv  43265  xlimpnfvlem2  43268  xlimpnfv  43269  climxlim2lem  43276  icccncfext  43318  fourierdlem64  43601  fourierdlem73  43610  etransclem35  43700  sge0tsms  43808  hoicvr  43976  hspmbllem2  44055  smflimlem2  44194  smflimlem4  44196