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

Theorem simpr1l 1226
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 769 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr1 1184 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1083
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 209  df-an 399  df-3an 1085
This theorem is referenced by:  oppccatid  16983  subccatid  17110  setccatid  17338  catccatid  17356  estrccatid  17376  xpccatid  17432  gsmsymgreqlem1  18552  dmdprdsplit  19163  neiptopnei  21734  neitr  21782  neitx  22209  tx1stc  22252  utop3cls  22854  metustsym  23159  ax5seg  26718  clwwlkccat  27762  3pthdlem1  27937  esumpcvgval  31332  esum2d  31347  ifscgr  33500  brofs2  33533  brifs2  33534  btwnconn1lem8  33550  btwnconn1lem12  33554  seglecgr12im  33566  unbdqndv2  33845  lhp2lt  37131  cdlemd1  37328  cdleme3b  37359  cdleme3c  37360  cdleme3e  37362  cdlemf2  37692  cdlemg4c  37742  cdlemn11pre  38340  dihmeetlem12N  38448  stoweidlem60  42339
  Copyright terms: Public domain W3C validator