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  28492  legov  28563  dfcgra2  28808  suppovss  32662  cyc3genpm  33121  elrgspnlem4  33212  rhmimaidl  33397  fedgmul  33644  zarclsun  33883  omssubadd  34313  circlemeth  34653  poimirlem29  37699  adantlllr  45146  supxrge  45447  xrralrecnnle  45491  rexabslelem  45526  limclner  45759  xlimmnfvlem2  45941  xlimmnfv  45942  xlimpnfvlem2  45945  xlimpnfv  45946  climxlim2lem  45953  icccncfext  45995  fourierdlem64  46278  fourierdlem73  46287  etransclem35  46377  sge0tsms  46488  hoicvr  46656  hspmbllem2  46735  smflimlem2  46880  smflimlem4  46882