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  8083  ttrcltr  9631  ttrclss  9635  dmttrcl  9636  ttrclselem2  9641  oppccatid  17643  subccatid  17771  setccatid  18009  catccatid  18031  estrccatid  18056  xpccatid  18112  kerf1ghm  19144  gsmsymgreqlem1  19327  nllyidm  23392  noinfbnd1lem5  27655  ax5seg  28901  3pthdlem1  30126  segconeq  35983  ifscgr  36017  brofs2  36050  brifs2  36051  idinside  36057  btwnconn1lem8  36067  btwnconn1lem12  36071  segcon2  36078  segletr  36087  outsidele  36105  unbdqndv2  36484  lplnexllnN  39543  paddasslem9  39807  pmodlem2  39826  lhp2lt  39980  cdlemc3  40172  cdlemc4  40173  cdlemd1  40177  cdleme3b  40208  cdleme3c  40209  cdleme42ke  40464  cdlemg4c  40591  clnbgrgrimlem  47918  ssccatid  49058  isthincd2  49423  mndtccatid  49573