Theorem simpr3l 1251

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  poxp2  8127  nosupbnd1lem5  27834  noinfbnd1lem5  27849  ax5seg  29197  axcont  29235  segconeq  36373  idinside  36447  btwnconn1lem10  36459  segletr  36477  cdlemc3  40829  cdlemc4  40830  cdleme1  40863  cdleme2  40864  cdleme3b  40865  cdleme3c  40866  cdleme3e  40868  cdleme27a  41003  stoweidlem56  46628  clnbgrgrimlem  48553