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  8162  nosupbnd1lem5  28074  noinfbnd1lem5  28089  ax5seg  29521  axcont  29559  segconeq  36867  idinside  36941  btwnconn1lem10  36953  segletr  36971  cdlemc3  41343  cdlemc4  41344  cdleme1  41377  cdleme2  41378  cdleme3b  41379  cdleme3c  41380  cdleme3e  41382  cdleme27a  41517  stoweidlem56  47159  clnbgrgrimlem  49124