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

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

Proof of Theorem simpr1r
StepHypRef Expression
1 simprr 772 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜓)
213ad2antr1 1185 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  oppccatid  16984  subccatid  17111  setccatid  17339  catccatid  17357  estrccatid  17377  xpccatid  17433  gsmsymgreqlem1  18554  dmdprdsplit  19166  neitr  21795  neitx  22222  tx1stc  22265  utop3cls  22867  metustsym  23172  clwwlkccat  27785  3pthdlem1  27959  archiabllem1  30882  esumpcvgval  31462  esum2d  31477  ifscgr  33633  btwnconn1lem8  33683  btwnconn1lem11  33686  btwnconn1lem12  33687  segletr  33703  broutsideof3  33715  unbdqndv2  33978  lhp2lt  37316  cdlemf2  37877  cdlemn11pre  38525  stoweidlem60  42745
 Copyright terms: Public domain W3C validator