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

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

Proof of Theorem simpr1r
StepHypRef Expression
1 simp1r 1084 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
21adantl 482 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  oppccatid  16300  subccatid  16427  setccatid  16655  catccatid  16673  estrccatid  16693  xpccatid  16749  gsmsymgreqlem1  17771  dmdprdsplit  18367  neitr  20894  neitx  21320  tx1stc  21363  utop3cls  21965  metustsym  22270  3pthdlem1  26890  frgrwopreg  27044  archiabllem1  29532  esumpcvgval  29921  esum2d  29936  ifscgr  31793  btwnconn1lem8  31843  btwnconn1lem11  31846  btwnconn1lem12  31847  segletr  31863  broutsideof3  31875  unbdqndv2  32144  lhp2lt  34767  cdlemf2  35330  cdlemn11pre  35979  stoweidlem60  39584
  Copyright terms: Public domain W3C validator