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  28536  legov  28607  dfcgra2  28852  suppovss  32695  cyc3genpm  33154  elrgspnlem4  33234  rhmimaidl  33439  fedgmul  33658  zarclsun  33830  omssubadd  34281  circlemeth  34633  poimirlem29  37635  adantlllr  44976  supxrge  45287  xrralrecnnle  45332  rexabslelem  45367  limclner  45606  xlimmnfvlem2  45788  xlimmnfv  45789  xlimpnfvlem2  45792  xlimpnfv  45793  climxlim2lem  45800  icccncfext  45842  fourierdlem64  46125  fourierdlem73  46134  etransclem35  46224  sge0tsms  46335  hoicvr  46503  hspmbllem2  46582  smflimlem2  46727  smflimlem4  46729