Theorem simpr2l 1239

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  poxp2  8090  ttrcltr  9635  ttrclss  9639  dmttrcl  9640  ttrclselem2  9645  oppccatid  17683  subccatid  17811  setccatid  18049  catccatid  18071  estrccatid  18096  xpccatid  18152  kerf1ghm  19220  gsmsymgreqlem1  19403  nllyidm  23479  noinfbnd1lem5  27716  ax5seg  29032  3pthdlem1  30259  segconeq  36245  ifscgr  36279  brofs2  36312  brifs2  36313  idinside  36319  btwnconn1lem8  36329  btwnconn1lem12  36333  segcon2  36340  segletr  36349  outsidele  36367  unbdqndv2  36824  lplnexllnN  40063  paddasslem9  40327  pmodlem2  40346  lhp2lt  40500  cdlemc3  40692  cdlemc4  40693  cdlemd1  40697  cdleme3b  40728  cdleme3c  40729  cdleme42ke  40984  cdlemg4c  41111  clnbgrgrimlem  48431  ssccatid  49569  isthincd2  49934  mndtccatid  50084