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  28535  legov  28606  dfcgra2  28851  suppovss  32709  cyc3genpm  33183  elrgspnlem4  33276  rhmimaidl  33462  fedgmul  33737  zarclsun  33976  omssubadd  34406  circlemeth  34746  poimirlem29  37789  adantlllr  45226  supxrge  45525  xrralrecnnle  45569  rexabslelem  45604  limclner  45837  xlimmnfvlem2  46019  xlimmnfv  46020  xlimpnfvlem2  46023  xlimpnfv  46024  climxlim2lem  46031  icccncfext  46073  fourierdlem64  46356  fourierdlem73  46365  etransclem35  46455  sge0tsms  46566  hoicvr  46734  hspmbllem2  46813  smflimlem2  46958  smflimlem4  46960