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

Theorem simpr1r 1112
 Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpr1r ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜓)

Proof of Theorem simpr1r
StepHypRef Expression
1 simp1r 1079 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
21adantl 481 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  oppccatid  16202  subccatid  16329  setccatid  16557  catccatid  16575  estrccatid  16595  xpccatid  16651  gsmsymgreqlem1  17673  dmdprdsplit  18269  neitr  20794  neitx  21220  tx1stc  21263  utop3cls  21865  metustsym  22170  frgrawopreg  26576  archiabllem1  29078  esumpcvgval  29467  esum2d  29482  ifscgr  31321  btwnconn1lem8  31371  btwnconn1lem11  31374  btwnconn1lem12  31375  segletr  31391  broutsideof3  31403  unbdqndv2  31672  lhp2lt  34305  cdlemf2  34868  cdlemn11pre  35517  stoweidlem60  38953  3pthdlem1  41331  frgrwopreg  41486
 Copyright terms: Public domain W3C validator