Theorem simpr2l 1229

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 769	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2antr2 1186	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  poxp2  8148  ttrcltr  9741  ttrclss  9745  dmttrcl  9746  ttrclselem2  9751  oppccatid  17704  subccatid  17835  setccatid  18076  catccatid  18098  estrccatid  18125  xpccatid  18182  kerf1ghm  19210  gsmsymgreqlem1  19397  nllyidm  23437  noinfbnd1lem5  27706  ax5seg  28821  3pthdlem1  30046  segconeq  35737  ifscgr  35771  brofs2  35804  brifs2  35805  idinside  35811  btwnconn1lem8  35821  btwnconn1lem12  35825  segcon2  35832  segletr  35841  outsidele  35859  unbdqndv2  36117  lplnexllnN  39167  paddasslem9  39431  pmodlem2  39450  lhp2lt  39604  cdlemc3  39796  cdlemc4  39797  cdlemd1  39801  cdleme3b  39832  cdleme3c  39833  cdleme42ke  40088  cdlemg4c  40215  isthincd2  48230  mndtccatid  48285