Theorem simpr3l 1122

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpr3l	⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑)

Proof of Theorem simpr3l

Step	Hyp	Ref	Expression
1		simp3l 1089	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	adantl 482	1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  ax5seg  25818  axcont  25856  nosupbnd1lem5  31858  segconeq  32117  idinside  32191  btwnconn1lem10  32203  segletr  32221  cdlemc3  35480  cdlemc4  35481  cdleme1  35514  cdleme2  35515  cdleme3b  35516  cdleme3c  35517  cdleme3e  35519  cdleme27a  35655  stoweidlem56  40273