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  28977  legov  29048  dfcgra2  29338  suppovss  33274  cyc3genpm  33713  elrgspnlem4  33806  rhmimaidl  33982  fedgmul  34263  zarclsun  34502  omssubadd  34932  circlemeth  35269  poimirlem29  38567  adantlllr  46055  supxrge  46349  xrralrecnnle  46393  rexabslelem  46427  limclner  46660  xlimmnfvlem2  46842  xlimmnfv  46843  xlimpnfvlem2  46846  xlimpnfv  46847  climxlim2lem  46854  icccncfext  46896  fourierdlem64  47179  fourierdlem73  47188  etransclem35  47278  sge0tsms  47389  hoicvr  47557  hspmbllem2  47636  smflimlem2  47781  smflimlem4  47783