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

Theorem simpr2l 1224
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 767 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr2 1181 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  oppccatid  16977  subccatid  17104  setccatid  17332  catccatid  17350  estrccatid  17370  xpccatid  17426  gsmsymgreqlem1  18487  kerf1ghm  19426  kerf1hrmOLD  19427  nllyidm  22025  ax5seg  26651  3pthdlem1  27870  segconeq  33368  ifscgr  33402  brofs2  33435  brifs2  33436  idinside  33442  btwnconn1lem8  33452  btwnconn1lem12  33456  segcon2  33463  segletr  33472  outsidele  33490  unbdqndv2  33747  lplnexllnN  36580  paddasslem9  36844  pmodlem2  36863  lhp2lt  37017  cdlemc3  37209  cdlemc4  37210  cdlemd1  37214  cdleme3b  37245  cdleme3c  37246  cdleme42ke  37501  cdlemg4c  37628
  Copyright terms: Public domain W3C validator