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 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  poxp2  8085  ttrcltr  9625  ttrclss  9629  dmttrcl  9630  ttrclselem2  9635  oppccatid  17642  subccatid  17770  setccatid  18008  catccatid  18030  estrccatid  18055  xpccatid  18111  kerf1ghm  19176  gsmsymgreqlem1  19359  nllyidm  23433  noinfbnd1lem5  27695  ax5seg  29011  3pthdlem1  30239  segconeq  36204  ifscgr  36238  brofs2  36271  brifs2  36272  idinside  36278  btwnconn1lem8  36288  btwnconn1lem12  36292  segcon2  36299  segletr  36308  outsidele  36326  unbdqndv2  36711  lplnexllnN  39820  paddasslem9  40084  pmodlem2  40103  lhp2lt  40257  cdlemc3  40449  cdlemc4  40450  cdlemd1  40454  cdleme3b  40485  cdleme3c  40486  cdleme42ke  40741  cdlemg4c  40868  clnbgrgrimlem  48175  ssccatid  49313  isthincd2  49678  mndtccatid  49828