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

Theorem simpr1l 1291
 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 1204 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  16580  subccatid  16707  setccatid  16935  catccatid  16953  estrccatid  16973  xpccatid  17029  gsmsymgreqlem1  18050  dmdprdsplit  18646  neiptopnei  21138  neitr  21186  neitx  21612  tx1stc  21655  utop3cls  22256  metustsym  22561  ax5seg  26017  3pthdlem1  27316  esumpcvgval  30449  esum2d  30464  ifscgr  32457  brofs2  32490  brifs2  32491  btwnconn1lem8  32507  btwnconn1lem12  32511  seglecgr12im  32523  unbdqndv2  32808  lhp2lt  35790  cdlemd1  35988  cdleme3b  36019  cdleme3c  36020  cdleme3e  36022  cdlemf2  36352  cdlemg4c  36402  cdlemn11pre  37001  dihmeetlem12N  37109  stoweidlem60  40780
 Copyright terms: Public domain W3C validator