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  8145  nosupbnd1lem5  27956  noinfbnd1lem5  27971  ax5seg  29403  axcont  29441  segconeq  36598  idinside  36672  btwnconn1lem10  36684  segletr  36702  cdlemc3  41074  cdlemc4  41075  cdleme1  41108  cdleme2  41109  cdleme3b  41110  cdleme3c  41111  cdleme3e  41113  cdleme27a  41248  stoweidlem56  46892  clnbgrgrimlem  48857