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

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
StepHypRef Expression
1 simprl 770 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr2 1190 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)
Colors of variables: wff setvar class
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  8076  ttrcltr  9657  ttrclss  9661  dmttrcl  9662  ttrclselem2  9667  oppccatid  17606  subccatid  17737  setccatid  17975  catccatid  17997  estrccatid  18024  xpccatid  18081  gsmsymgreqlem1  19217  kerf1ghm  20184  nllyidm  22856  noinfbnd1lem5  27091  ax5seg  27929  3pthdlem1  29150  segconeq  34641  ifscgr  34675  brofs2  34708  brifs2  34709  idinside  34715  btwnconn1lem8  34725  btwnconn1lem12  34729  segcon2  34736  segletr  34745  outsidele  34763  unbdqndv2  35020  lplnexllnN  38073  paddasslem9  38337  pmodlem2  38356  lhp2lt  38510  cdlemc3  38702  cdlemc4  38703  cdlemd1  38707  cdleme3b  38738  cdleme3c  38739  cdleme42ke  38994  cdlemg4c  39121  isthincd2  47144  mndtccatid  47199
  Copyright terms: Public domain W3C validator