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

Theorem simpr1l 1227
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)
Assertion
Ref Expression
simpr1l ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜑)

Proof of Theorem simpr1l
StepHypRef Expression
1 simprl 768 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr1 1185 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  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 396  df-3an 1086
This theorem is referenced by:  poxp2  8124  poxp3  8131  oppccatid  17666  subccatid  17797  setccatid  18038  catccatid  18060  estrccatid  18087  xpccatid  18144  gsmsymgreqlem1  19342  dmdprdsplit  19961  neiptopnei  22960  neitr  23008  neitx  23435  tx1stc  23478  utop3cls  24080  metustsym  24388  ax5seg  28668  clwwlkccat  29715  3pthdlem1  29889  esumpcvgval  33568  esum2d  33583  ifscgr  35512  brofs2  35545  brifs2  35546  btwnconn1lem8  35562  btwnconn1lem12  35566  seglecgr12im  35578  unbdqndv2  35878  lhp2lt  39366  cdlemd1  39563  cdleme3b  39594  cdleme3c  39595  cdleme3e  39597  cdlemf2  39927  cdlemg4c  39977  cdlemn11pre  40575  dihmeetlem12N  40683  stoweidlem60  45286  isthincd2  47870  mndtccatid  47925
  Copyright terms: Public domain W3C validator