Theorem simpr3l 1253

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpr3l	⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑)

Proof of Theorem simpr3l

Step	Hyp	Ref	Expression
1		simprl 783	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2antr3 1209	1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

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  df-3an 1105

This theorem is used by:  poxp2  8144  nosupbnd1lem5  28051  noinfbnd1lem5  28066  ax5seg  29498  axcont  29536  segconeq  36745  idinside  36819  btwnconn1lem10  36831  segletr  36849  cdlemc3  41218  cdlemc4  41219  cdleme1  41252  cdleme2  41253  cdleme3b  41254  cdleme3c  41255  cdleme3e  41257  cdleme27a  41392  stoweidlem56  47010  clnbgrgrimlem  48975