Theorem adantl3r 747

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 712	. 2 ⊢ (((𝜑 ∧ 𝜂) ∧ 𝜓) → (𝜑 ∧ 𝜓))
3		adantl3r.1	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylanl1 677	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  752  iscgrglt  28033  legov  28104  dfcgra2  28349  suppovss  32174  cyc3genpm  32582  rhmimaidl  32825  fedgmul  33005  zarclsun  33149  omssubadd  33598  circlemeth  33951  poimirlem29  36821  adantlllr  44026  supxrge  44347  xrralrecnnle  44392  rexabslelem  44427  limclner  44666  xlimmnfvlem2  44848  xlimmnfv  44849  xlimpnfvlem2  44852  xlimpnfv  44853  climxlim2lem  44860  icccncfext  44902  fourierdlem64  45185  fourierdlem73  45194  etransclem35  45284  sge0tsms  45395  hoicvr  45563  hspmbllem2  45642  smflimlem2  45787  smflimlem4  45789