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  28522  legov  28593  dfcgra2  28838  suppovss  32690  cyc3genpm  33172  elrgspnlem4  33249  rhmimaidl  33460  fedgmul  33682  zarclsun  33869  omssubadd  34302  circlemeth  34655  poimirlem29  37656  adantlllr  45044  supxrge  45349  xrralrecnnle  45394  rexabslelem  45429  limclner  45666  xlimmnfvlem2  45848  xlimmnfv  45849  xlimpnfvlem2  45852  xlimpnfv  45853  climxlim2lem  45860  icccncfext  45902  fourierdlem64  46185  fourierdlem73  46194  etransclem35  46284  sge0tsms  46395  hoicvr  46563  hspmbllem2  46642  smflimlem2  46787  smflimlem4  46789