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

Theorem simpr1l 1267
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 811 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr1 1180 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  oppccatid  16551  subccatid  16678  setccatid  16906  catccatid  16924  estrccatid  16944  xpccatid  17000  gsmsymgreqlem1  18021  dmdprdsplit  18617  neiptopnei  21109  neitr  21157  neitx  21583  tx1stc  21626  utop3cls  22227  metustsym  22532  ax5seg  25988  3pthdlem1  27287  esumpcvgval  30420  esum2d  30435  ifscgr  32428  brofs2  32461  brifs2  32462  btwnconn1lem8  32478  btwnconn1lem12  32482  seglecgr12im  32494  unbdqndv2  32779  lhp2lt  35759  cdlemd1  35957  cdleme3b  35988  cdleme3c  35989  cdleme3e  35991  cdlemf2  36321  cdlemg4c  36371  cdlemn11pre  36970  dihmeetlem12N  37078  stoweidlem60  40749
  Copyright terms: Public domain W3C validator