Theorem simpr3l 1233

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

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

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ax5seg  27306  axcont  27344  poxp2  33790  nosupbnd1lem5  33915  noinfbnd1lem5  33930  segconeq  34312  idinside  34386  btwnconn1lem10  34398  segletr  34416  cdlemc3  38207  cdlemc4  38208  cdleme1  38241  cdleme2  38242  cdleme3b  38243  cdleme3c  38244  cdleme3e  38246  cdleme27a  38381  stoweidlem56  43597