Theorem simpr3l 1235

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 1191	1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑)

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

This theorem is referenced by:  poxp2  8085  nosupbnd1lem5  27680  noinfbnd1lem5  27695  ax5seg  29011  axcont  29049  segconeq  36204  idinside  36278  btwnconn1lem10  36290  segletr  36308  cdlemc3  40449  cdlemc4  40450  cdleme1  40483  cdleme2  40484  cdleme3b  40485  cdleme3c  40486  cdleme3e  40488  cdleme27a  40623  stoweidlem56  46296  clnbgrgrimlem  48175