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

Theorem simpr2l 1226
 Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)
Assertion
Ref Expression
simpr2l ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)

Proof of Theorem simpr2l
StepHypRef Expression
1 simprl 769 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr2 1183 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1081 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 209  df-an 399  df-3an 1083 This theorem is referenced by:  oppccatid  16981  subccatid  17108  setccatid  17336  catccatid  17354  estrccatid  17374  xpccatid  17430  gsmsymgreqlem1  18550  kerf1ghm  19489  kerf1hrmOLD  19490  nllyidm  22089  ax5seg  26716  3pthdlem1  27935  segconeq  33464  ifscgr  33498  brofs2  33531  brifs2  33532  idinside  33538  btwnconn1lem8  33548  btwnconn1lem12  33552  segcon2  33559  segletr  33568  outsidele  33586  unbdqndv2  33843  lplnexllnN  36692  paddasslem9  36956  pmodlem2  36975  lhp2lt  37129  cdlemc3  37321  cdlemc4  37322  cdlemd1  37326  cdleme3b  37357  cdleme3c  37358  cdleme42ke  37613  cdlemg4c  37740
 Copyright terms: Public domain W3C validator