Theorem adantl3r 762

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  adantl4r  767  ad5ant134  1392  ad5ant135  1394  iscgrglt  28783  legov  28854  dfcgra2  29141  suppovss  33026  cyc3genpm  33472  elrgspnlem4  33565  rhmimaidl  33740  fedgmul  34021  zarclsun  34260  omssubadd  34690  circlemeth  35027  poimirlem29  38320  adantlllr  45779  supxrge  46074  xrralrecnnle  46118  rexabslelem  46152  limclner  46385  xlimmnfvlem2  46567  xlimmnfv  46568  xlimpnfvlem2  46571  xlimpnfv  46572  climxlim2lem  46579  icccncfext  46621  fourierdlem64  46904  fourierdlem73  46913  etransclem35  47003  sge0tsms  47114  hoicvr  47282  hspmbllem2  47361  smflimlem2  47506  smflimlem4  47508