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  28494  legov  28565  dfcgra2  28810  suppovss  32654  cyc3genpm  33124  elrgspnlem4  33212  rhmimaidl  33396  fedgmul  33620  zarclsun  33853  omssubadd  34284  circlemeth  34624  poimirlem29  37636  adantlllr  45026  supxrge  45327  xrralrecnnle  45372  rexabslelem  45407  limclner  45642  xlimmnfvlem2  45824  xlimmnfv  45825  xlimpnfvlem2  45828  xlimpnfv  45829  climxlim2lem  45836  icccncfext  45878  fourierdlem64  46161  fourierdlem73  46170  etransclem35  46260  sge0tsms  46371  hoicvr  46539  hspmbllem2  46618  smflimlem2  46763  smflimlem4  46765