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 771 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr2 1190 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  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 210  df-an 400  df-3an 1090
This theorem is referenced by:  oppccatid  17096  subccatid  17224  setccatid  17459  catccatid  17481  estrccatid  17501  xpccatid  17557  gsmsymgreqlem1  18679  kerf1ghm  19620  nllyidm  22243  ax5seg  26887  3pthdlem1  28104  poxp2  33406  noinfbnd1lem5  33576  segconeq  33958  ifscgr  33992  brofs2  34025  brifs2  34026  idinside  34032  btwnconn1lem8  34042  btwnconn1lem12  34046  segcon2  34053  segletr  34062  outsidele  34080  unbdqndv2  34337  lplnexllnN  37224  paddasslem9  37488  pmodlem2  37507  lhp2lt  37661  cdlemc3  37853  cdlemc4  37854  cdlemd1  37858  cdleme3b  37889  cdleme3c  37890  cdleme42ke  38145  cdlemg4c  38272  isthincd2  45822  mndtccatid  45857
  Copyright terms: Public domain W3C validator