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  8162  ttrcltr  9720  ttrclss  9724  dmttrcl  9725  ttrclselem2  9730  oppccatid  17898  subccatid  18026  setccatid  18264  catccatid  18286  estrccatid  18311  xpccatid  18367  kerf1ghm  19466  gsmsymgreqlem1  19649  nllyidm  23813  noinfbnd1lem5  28089  ax5seg  29521  3pthdlem1  30770  segconeq  36867  ifscgr  36901  brofs2  36934  brifs2  36935  idinside  36941  btwnconn1lem8  36951  btwnconn1lem12  36955  segcon2  36962  segletr  36971  outsidele  36989  unbdqndv2  37469  lplnexllnN  40714  paddasslem9  40978  pmodlem2  40997  lhp2lt  41151  cdlemc3  41343  cdlemc4  41344  cdlemd1  41348  cdleme3b  41379  cdleme3c  41380  cdleme42ke  41635  cdlemg4c  41762  clnbgrgrimlem  49124  ssccatid  50279  isthincd2  50665  mndtccatid  50818