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  8125  ttrcltr  9676  ttrclss  9680  dmttrcl  9681  ttrclselem2  9686  oppccatid  17687  subccatid  17815  setccatid  18053  catccatid  18075  estrccatid  18100  xpccatid  18156  kerf1ghm  19186  gsmsymgreqlem1  19367  nllyidm  23383  noinfbnd1lem5  27646  ax5seg  28872  3pthdlem1  30100  segconeq  36005  ifscgr  36039  brofs2  36072  brifs2  36073  idinside  36079  btwnconn1lem8  36089  btwnconn1lem12  36093  segcon2  36100  segletr  36109  outsidele  36127  unbdqndv2  36506  lplnexllnN  39565  paddasslem9  39829  pmodlem2  39848  lhp2lt  40002  cdlemc3  40194  cdlemc4  40195  cdlemd1  40199  cdleme3b  40230  cdleme3c  40231  cdleme42ke  40486  cdlemg4c  40613  clnbgrgrimlem  47937  ssccatid  49065  isthincd2  49430  mndtccatid  49580