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  8190  nosupbnd1lem5  28102  noinfbnd1lem5  28117  ax5seg  29549  axcont  29587  segconeq  36966  idinside  37040  btwnconn1lem10  37052  segletr  37070  cdlemc3  41453  cdlemc4  41454  cdleme1  41487  cdleme2  41488  cdleme3b  41489  cdleme3c  41490  cdleme3e  41492  cdleme27a  41627  stoweidlem56  47281  clnbgrgrimlem  49246