Theorem adantl3r 751

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  adantl4r  756  iscgrglt  28582  legov  28653  dfcgra2  28898  suppovss  32754  cyc3genpm  33213  elrgspnlem4  33306  rhmimaidl  33492  fedgmul  33775  zarclsun  34014  omssubadd  34444  circlemeth  34784  poimirlem29  37970  adantlllr  45470  supxrge  45768  xrralrecnnle  45812  rexabslelem  45846  limclner  46079  xlimmnfvlem2  46261  xlimmnfv  46262  xlimpnfvlem2  46265  xlimpnfv  46266  climxlim2lem  46273  icccncfext  46315  fourierdlem64  46598  fourierdlem73  46607  etransclem35  46697  sge0tsms  46808  hoicvr  46976  hspmbllem2  47055  smflimlem2  47200  smflimlem4  47202