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  8148  nosupbnd1lem5  27913  noinfbnd1lem5  27928  ax5seg  29325  axcont  29363  segconeq  36523  idinside  36597  btwnconn1lem10  36609  segletr  36627  cdlemc3  41008  cdlemc4  41009  cdleme1  41042  cdleme2  41043  cdleme3b  41044  cdleme3c  41045  cdleme3e  41047  cdleme27a  41182  stoweidlem56  46811  clnbgrgrimlem  48739