Theorem adantl3r 803

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		adantl3r.1	. . . 4 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
2	1	ex 449	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜃 → 𝜏))
3	2	adantllr 757	. 2 ⊢ ((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) → (𝜃 → 𝜏))
4	3	imp 444	1 ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  adantl4r  804  ad5ant1345  1473  iscgrglt  25608  legov  25679  dfcgra2  25920  omssubadd  30671  circlemeth  31027  poimirlem29  33751  adantlllr  39698  supxrge  40052  xrralrecnnle  40100  rexabslelem  40143  limclner  40386  xlimmnfvlem2  40562  xlimmnfv  40563  xlimpnfvlem2  40566  xlimpnfv  40567  climxlim2lem  40574  icccncfext  40603  fourierdlem64  40890  fourierdlem73  40899  etransclem35  40989  sge0tsms  41100  hoicvr  41268  hspmbllem2  41347  smflimlem2  41486  smflimlem4  41488