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

Theorem simpr1l 1230
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 1188 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  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 206  df-an 397  df-3an 1089
This theorem is referenced by:  poxp2  8128  poxp3  8135  oppccatid  17664  subccatid  17795  setccatid  18033  catccatid  18055  estrccatid  18082  xpccatid  18139  gsmsymgreqlem1  19297  dmdprdsplit  19916  neiptopnei  22635  neitr  22683  neitx  23110  tx1stc  23153  utop3cls  23755  metustsym  24063  ax5seg  28193  clwwlkccat  29240  3pthdlem1  29414  esumpcvgval  33071  esum2d  33086  ifscgr  35011  brofs2  35044  brifs2  35045  btwnconn1lem8  35061  btwnconn1lem12  35065  seglecgr12im  35077  unbdqndv2  35382  lhp2lt  38867  cdlemd1  39064  cdleme3b  39095  cdleme3c  39096  cdleme3e  39098  cdlemf2  39428  cdlemg4c  39478  cdlemn11pre  40076  dihmeetlem12N  40184  stoweidlem60  44766  isthincd2  47648  mndtccatid  47703
  Copyright terms: Public domain W3C validator