MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpr2l Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 simprl 769 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr2 1186 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator