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

Theorem simpr1r 1232
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 773 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜓)
213ad2antr1 1189 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  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 207  df-an 396  df-3an 1089
This theorem is referenced by:  poxp2  8168  oppccatid  17762  subccatid  17891  setccatid  18129  catccatid  18151  estrccatid  18176  xpccatid  18233  gsmsymgreqlem1  19448  dmdprdsplit  20067  neitr  23188  neitx  23615  tx1stc  23658  utop3cls  24260  metustsym  24568  clwwlkccat  30009  3pthdlem1  30183  archiabllem1  33200  esumpcvgval  34079  esum2d  34094  ifscgr  36045  btwnconn1lem8  36095  btwnconn1lem11  36098  btwnconn1lem12  36099  segletr  36115  broutsideof3  36127  unbdqndv2  36512  lhp2lt  40003  cdlemf2  40564  cdlemn11pre  41212  stoweidlem60  46075  isthincd2  49086  mndtccatid  49184
  Copyright terms: Public domain W3C validator