Theorem adantl3r 756

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 721	. 2 ⊢ (((𝜑 ∧ 𝜂) ∧ 𝜓) → (𝜑 ∧ 𝜓))
3		adantl3r.1	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylanl1 686	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  761  iscgrglt  28600  legov  28671  dfcgra2  28916  suppovss  32773  cyc3genpm  33233  elrgspnlem4  33326  rhmimaidl  33515  fedgmul  33815  zarclsun  34054  omssubadd  34484  circlemeth  34824  poimirlem29  38016  adantlllr  45487  supxrge  45783  xrralrecnnle  45827  rexabslelem  45861  limclner  46094  xlimmnfvlem2  46276  xlimmnfv  46277  xlimpnfvlem2  46280  xlimpnfv  46281  climxlim2lem  46288  icccncfext  46330  fourierdlem64  46613  fourierdlem73  46622  etransclem35  46712  sge0tsms  46823  hoicvr  46991  hspmbllem2  47070  smflimlem2  47215  smflimlem4  47217