Theorem simpr3l 1232

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  ax5seg  27209  axcont  27247  poxp2  33717  nosupbnd1lem5  33842  noinfbnd1lem5  33857  segconeq  34239  idinside  34313  btwnconn1lem10  34325  segletr  34343  cdlemc3  38134  cdlemc4  38135  cdleme1  38168  cdleme2  38169  cdleme3b  38170  cdleme3c  38171  cdleme3e  38173  cdleme27a  38308  stoweidlem56  43487