Theorem simpr3l 1241

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 776	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2antr3 1197	1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094

This theorem is referenced by:  poxp2  8090  nosupbnd1lem5  27701  noinfbnd1lem5  27716  ax5seg  29032  axcont  29070  segconeq  36245  idinside  36319  btwnconn1lem10  36331  segletr  36349  cdlemc3  40692  cdlemc4  40693  cdleme1  40726  cdleme2  40727  cdleme3b  40728  cdleme3c  40729  cdleme3e  40731  cdleme27a  40866  stoweidlem56  46506  clnbgrgrimlem  48431