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

Theorem simpr1l 1262
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 761 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr1 1196 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  dmdprdsplit  18833  neiptopnei  21344  neitr  21392  neitx  21819  tx1stc  21862  utop3cls  22463  metustsym  22768  ax5seg  26287  3pthdlem1  27567  esumpcvgval  30738  esum2d  30753  ifscgr  32740  brofs2  32773  brifs2  32774  btwnconn1lem8  32790  btwnconn1lem12  32794  seglecgr12im  32806  unbdqndv2  33084  lhp2lt  36157  cdlemd1  36354  cdleme3b  36385  cdleme3c  36386  cdleme3e  36388  cdlemf2  36718  cdlemg4c  36768  cdlemn11pre  37366  dihmeetlem12N  37474  stoweidlem60  41208
  Copyright terms: Public domain W3C validator