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  28859  legov  28930  dfcgra2  29220  suppovss  33156  cyc3genpm  33595  elrgspnlem4  33688  rhmimaidl  33863  fedgmul  34144  zarclsun  34383  omssubadd  34814  circlemeth  35151  poimirlem29  38401  adantlllr  45876  supxrge  46171  xrralrecnnle  46215  rexabslelem  46249  limclner  46482  xlimmnfvlem2  46664  xlimmnfv  46665  xlimpnfvlem2  46668  xlimpnfv  46669  climxlim2lem  46676  icccncfext  46718  fourierdlem64  47001  fourierdlem73  47010  etransclem35  47100  sge0tsms  47211  hoicvr  47379  hspmbllem2  47458  smflimlem2  47603  smflimlem4  47605