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 399

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 210  df-an 400

This theorem is referenced by:  adantl4r  755  iscgrglt  26605  legov  26676  dfcgra2  26921  suppovss  30737  cyc3genpm  31138  rhmimaidl  31323  fedgmul  31426  zarclsun  31534  omssubadd  31979  circlemeth  32332  poimirlem29  35543  adantlllr  42256  supxrge  42550  xrralrecnnle  42595  rexabslelem  42631  limclner  42867  xlimmnfvlem2  43049  xlimmnfv  43050  xlimpnfvlem2  43053  xlimpnfv  43054  climxlim2lem  43061  icccncfext  43103  fourierdlem64  43386  fourierdlem73  43395  etransclem35  43485  sge0tsms  43593  hoicvr  43761  hspmbllem2  43840  smflimlem2  43979  smflimlem4  43981