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  28196  3pthdlem1  29417  segconeq  34982  ifscgr  35016  brofs2  35049  brifs2  35050  idinside  35056  btwnconn1lem8  35066  btwnconn1lem12  35070  segcon2  35077  segletr  35086  outsidele  35104  unbdqndv2  35387  lplnexllnN  38435  paddasslem9  38699  pmodlem2  38718  lhp2lt  38872  cdlemc3  39064  cdlemc4  39065  cdlemd1  39069  cdleme3b  39100  cdleme3c  39101  cdleme42ke  39356  cdlemg4c  39483  isthincd2  47658  mndtccatid  47713