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  28441  legov  28512  dfcgra2  28757  suppovss  32604  cyc3genpm  33109  elrgspnlem4  33196  rhmimaidl  33403  fedgmul  33627  zarclsun  33860  omssubadd  34291  circlemeth  34631  poimirlem29  37643  adantlllr  45033  supxrge  45334  xrralrecnnle  45379  rexabslelem  45414  limclner  45649  xlimmnfvlem2  45831  xlimmnfv  45832  xlimpnfvlem2  45835  xlimpnfv  45836  climxlim2lem  45843  icccncfext  45885  fourierdlem64  46168  fourierdlem73  46177  etransclem35  46267  sge0tsms  46378  hoicvr  46546  hspmbllem2  46625  smflimlem2  46770  smflimlem4  46772