Theorem simpr2l 1233

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  poxp2  8129  ttrcltr  9711  ttrclss  9715  dmttrcl  9716  ttrclselem2  9721  oppccatid  17665  subccatid  17796  setccatid  18034  catccatid  18056  estrccatid  18083  xpccatid  18140  gsmsymgreqlem1  19298  kerf1ghm  20282  nllyidm  22993  noinfbnd1lem5  27230  ax5seg  28227  3pthdlem1  29448  segconeq  35013  ifscgr  35047  brofs2  35080  brifs2  35081  idinside  35087  btwnconn1lem8  35097  btwnconn1lem12  35101  segcon2  35108  segletr  35117  outsidele  35135  unbdqndv2  35435  lplnexllnN  38483  paddasslem9  38747  pmodlem2  38766  lhp2lt  38920  cdlemc3  39112  cdlemc4  39113  cdlemd1  39117  cdleme3b  39148  cdleme3c  39149  cdleme42ke  39404  cdlemg4c  39531  isthincd2  47706  mndtccatid  47761