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

Theorem simpr1l 1231
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 770 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr1 1189 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  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 206  df-an 398  df-3an 1090
This theorem is referenced by:  poxp2  8076  poxp3  8083  oppccatid  17606  subccatid  17737  setccatid  17975  catccatid  17997  estrccatid  18024  xpccatid  18081  gsmsymgreqlem1  19217  dmdprdsplit  19831  neiptopnei  22499  neitr  22547  neitx  22974  tx1stc  23017  utop3cls  23619  metustsym  23927  ax5seg  27929  clwwlkccat  28976  3pthdlem1  29150  esumpcvgval  32734  esum2d  32749  ifscgr  34675  brofs2  34708  brifs2  34709  btwnconn1lem8  34725  btwnconn1lem12  34729  seglecgr12im  34741  unbdqndv2  35020  lhp2lt  38510  cdlemd1  38707  cdleme3b  38738  cdleme3c  38739  cdleme3e  38741  cdlemf2  39071  cdlemg4c  39121  cdlemn11pre  39719  dihmeetlem12N  39827  stoweidlem60  44387  isthincd2  47144  mndtccatid  47199
  Copyright terms: Public domain W3C validator