Theorem adantl3r 746

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 711	. 2 ⊢ (((𝜑 ∧ 𝜂) ∧ 𝜓) → (𝜑 ∧ 𝜓))
3		adantl3r.1	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylanl1 676	1 ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  adantl4r  751  iscgrglt  25987  legov  26058  dfcgra2  26303  suppovss  30121  cyc3genpm  30437  fedgmul  30636  omssubadd  31180  circlemeth  31533  poimirlem29  34477  adantlllr  40861  supxrge  41172  xrralrecnnle  41219  rexabslelem  41259  limclner  41499  xlimmnfvlem2  41681  xlimmnfv  41682  xlimpnfvlem2  41685  xlimpnfv  41686  climxlim2lem  41693  icccncfext  41737  fourierdlem64  42023  fourierdlem73  42032  etransclem35  42122  sge0tsms  42230  hoicvr  42398  hspmbllem2  42477  smflimlem2  42616  smflimlem4  42618