Theorem simpr3l 1234

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1087

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 398  df-3an 1089

This theorem is referenced by:  nosupbnd1lem5  26970  noinfbnd1lem5  26985  ax5seg  27661  axcont  27699  poxp2  34136  segconeq  34451  idinside  34525  btwnconn1lem10  34537  segletr  34555  cdlemc3  38512  cdlemc4  38513  cdleme1  38546  cdleme2  38547  cdleme3b  38548  cdleme3c  38549  cdleme3e  38551  cdleme27a  38686  stoweidlem56  43985