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  8145  ttrcltr  9699  ttrclss  9703  dmttrcl  9704  ttrclselem2  9709  oppccatid  17813  subccatid  17941  setccatid  18179  catccatid  18201  estrccatid  18226  xpccatid  18282  kerf1ghm  19380  gsmsymgreqlem1  19563  nllyidm  23721  noinfbnd1lem5  27971  ax5seg  29403  3pthdlem1  30652  segconeq  36598  ifscgr  36632  brofs2  36665  brifs2  36666  idinside  36672  btwnconn1lem8  36682  btwnconn1lem12  36686  segcon2  36693  segletr  36702  outsidele  36720  unbdqndv2  37216  lplnexllnN  40445  paddasslem9  40709  pmodlem2  40728  lhp2lt  40882  cdlemc3  41074  cdlemc4  41075  cdlemd1  41079  cdleme3b  41110  cdleme3c  41111  cdleme42ke  41366  cdlemg4c  41493  clnbgrgrimlem  48857  ssccatid  50006  isthincd2  50371  mndtccatid  50521