Theorem adantl3r 763

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 23	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2	1	adantlr 728	. 2 ⊢ (((𝜑 ∧ 𝜂) ∧ 𝜓) → (𝜑 ∧ 𝜓))
3		adantl3r.1	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylanl1 693	1 ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  adantl4r  768  ad5ant134  1392  ad5ant135  1394  iscgrglt  28978  legov  29049  dfcgra2  29339  suppovss  33275  cyc3genpm  33714  elrgspnlem4  33807  rhmimaidl  33983  fedgmul  34264  zarclsun  34503  omssubadd  34933  circlemeth  35270  poimirlem29  38569  adantlllr  46057  supxrge  46351  xrralrecnnle  46395  rexabslelem  46429  limclner  46662  xlimmnfvlem2  46844  xlimmnfv  46845  xlimpnfvlem2  46848  xlimpnfv  46849  climxlim2lem  46856  icccncfext  46898  fourierdlem64  47181  fourierdlem73  47190  etransclem35  47280  sge0tsms  47391  hoicvr  47559  hspmbllem2  47638  smflimlem2  47783  smflimlem4  47785