Theorem adantl3r 749

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 714	. 2 ⊢ (((𝜑 ∧ 𝜂) ∧ 𝜓) → (𝜑 ∧ 𝜓))
3		adantl3r.1	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylanl1 679	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  754  iscgrglt  28540  legov  28611  dfcgra2  28856  suppovss  32697  cyc3genpm  33145  rhmimaidl  33425  fedgmul  33644  zarclsun  33816  omssubadd  34265  circlemeth  34617  poimirlem29  37609  adantlllr  44939  supxrge  45253  xrralrecnnle  45298  rexabslelem  45333  limclner  45572  xlimmnfvlem2  45754  xlimmnfv  45755  xlimpnfvlem2  45758  xlimpnfv  45759  climxlim2lem  45766  icccncfext  45808  fourierdlem64  46091  fourierdlem73  46100  etransclem35  46190  sge0tsms  46301  hoicvr  46469  hspmbllem2  46548  smflimlem2  46693  smflimlem4  46695