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 771 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr1 1189 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  poxp2  8168  poxp3  8175  oppccatid  17762  subccatid  17891  setccatid  18129  catccatid  18151  estrccatid  18176  xpccatid  18233  gsmsymgreqlem1  19448  dmdprdsplit  20067  neiptopnei  23140  neitr  23188  neitx  23615  tx1stc  23658  utop3cls  24260  metustsym  24568  ax5seg  28953  clwwlkccat  30009  3pthdlem1  30183  esumpcvgval  34079  esum2d  34094  ifscgr  36045  brofs2  36078  brifs2  36079  btwnconn1lem8  36095  btwnconn1lem12  36099  seglecgr12im  36111  unbdqndv2  36512  lhp2lt  40003  cdlemd1  40200  cdleme3b  40231  cdleme3c  40232  cdleme3e  40234  cdlemf2  40564  cdlemg4c  40614  cdlemn11pre  41212  dihmeetlem12N  41320  stoweidlem60  46075  isthincd2  49086  mndtccatid  49184
  Copyright terms: Public domain W3C validator