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  28836  legov  28907  dfcgra2  29194  suppovss  33099  cyc3genpm  33538  elrgspnlem4  33631  rhmimaidl  33806  fedgmul  34087  zarclsun  34326  omssubadd  34757  circlemeth  35094  poimirlem29  38359  adantlllr  45819  supxrge  46114  xrralrecnnle  46158  rexabslelem  46192  limclner  46425  xlimmnfvlem2  46607  xlimmnfv  46608  xlimpnfvlem2  46611  xlimpnfv  46612  climxlim2lem  46619  icccncfext  46661  fourierdlem64  46944  fourierdlem73  46953  etransclem35  47043  sge0tsms  47154  hoicvr  47322  hspmbllem2  47401  smflimlem2  47546  smflimlem4  47548