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  28599  legov  28670  dfcgra2  28915  suppovss  32772  cyc3genpm  33231  elrgspnlem4  33324  rhmimaidl  33510  fedgmul  33794  zarclsun  34033  omssubadd  34463  circlemeth  34803  poimirlem29  37987  adantlllr  45491  supxrge  45789  xrralrecnnle  45833  rexabslelem  45867  limclner  46100  xlimmnfvlem2  46282  xlimmnfv  46283  xlimpnfvlem2  46286  xlimpnfv  46287  climxlim2lem  46294  icccncfext  46336  fourierdlem64  46619  fourierdlem73  46628  etransclem35  46718  sge0tsms  46829  hoicvr  46997  hspmbllem2  47076  smflimlem2  47221  smflimlem4  47223