Theorem simpr2l 1251

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

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

Proof of Theorem simpr2l

Step	Hyp	Ref	Expression
1		simprl 783	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2antr2 1208	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp2  8148  ttrcltr  9695  ttrclss  9699  dmttrcl  9700  ttrclselem2  9705  oppccatid  17800  subccatid  17928  setccatid  18166  catccatid  18188  estrccatid  18213  xpccatid  18269  kerf1ghm  19348  gsmsymgreqlem1  19531  nllyidm  23683  noinfbnd1lem5  27928  ax5seg  29325  3pthdlem1  30552  segconeq  36523  ifscgr  36557  brofs2  36590  brifs2  36591  idinside  36597  btwnconn1lem8  36607  btwnconn1lem12  36611  segcon2  36618  segletr  36627  outsidele  36645  unbdqndv2  37141  lplnexllnN  40379  paddasslem9  40643  pmodlem2  40662  lhp2lt  40816  cdlemc3  41008  cdlemc4  41009  cdlemd1  41013  cdleme3b  41044  cdleme3c  41045  cdleme42ke  41300  cdlemg4c  41427  clnbgrgrimlem  48739  ssccatid  49891  isthincd2  50256  mndtccatid  50406