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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  poxp2  8184  nosupbnd1lem5  27775  noinfbnd1lem5  27790  ax5seg  28971  axcont  29009  segconeq  35974  idinside  36048  btwnconn1lem10  36060  segletr  36078  cdlemc3  40150  cdlemc4  40151  cdleme1  40184  cdleme2  40185  cdleme3b  40186  cdleme3c  40187  cdleme3e  40189  cdleme27a  40324  stoweidlem56  45977  clnbgrgrimlem  47785