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

Theorem simpr2l 1266
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 761 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr2 1197 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1071
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 199  df-an 387  df-3an 1073
This theorem is referenced by:  oppccatid  16764  subccatid  16891  setccatid  17119  catccatid  17137  estrccatid  17157  xpccatid  17214  gsmsymgreqlem1  18233  kerf1ghm  19134  kerf1hrmOLD  19135  nllyidm  21701  ax5seg  26287  3pthdlem1  27581  segconeq  32720  ifscgr  32754  brofs2  32787  brifs2  32788  idinside  32794  btwnconn1lem8  32804  btwnconn1lem12  32808  segcon2  32815  segletr  32824  outsidele  32842  unbdqndv2  33098  lplnexllnN  35712  paddasslem9  35976  pmodlem2  35995  lhp2lt  36149  cdlemc3  36341  cdlemc4  36342  cdlemd1  36346  cdleme3b  36377  cdleme3c  36378  cdleme42ke  36633  cdlemg4c  36760
  Copyright terms: Public domain W3C validator