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  28493  legov  28564  dfcgra2  28809  suppovss  32658  cyc3genpm  33163  elrgspnlem4  33240  rhmimaidl  33447  fedgmul  33671  zarclsun  33901  omssubadd  34332  circlemeth  34672  poimirlem29  37673  adantlllr  45063  supxrge  45365  xrralrecnnle  45410  rexabslelem  45445  limclner  45680  xlimmnfvlem2  45862  xlimmnfv  45863  xlimpnfvlem2  45866  xlimpnfv  45867  climxlim2lem  45874  icccncfext  45916  fourierdlem64  46199  fourierdlem73  46208  etransclem35  46298  sge0tsms  46409  hoicvr  46577  hspmbllem2  46656  smflimlem2  46801  smflimlem4  46803