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

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

Proof of Theorem simplr3
StepHypRef Expression
1 simpr3 1089 . 2 ((𝜃 ∧ (𝜑𝜓𝜒)) → 𝜒)
21adantr 480 1 (((𝜃 ∧ (𝜑𝜓𝜒)) ∧ 𝜏) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  soltmin  5567  frfi  8246  wemappo  8495  iccsplit  12343  ccatswrd  13502  swrdccat3  13538  modfsummods  14569  pcdvdstr  15627  vdwlem12  15743  cshwsidrepswmod0  15848  iscatd2  16389  oppccomfpropd  16434  initoeu2lem0  16710  resssetc  16789  resscatc  16802  yonedalem4c  16964  mod1ile  17152  mod2ile  17153  prdsmndd  17370  grprcan  17502  mulgnn0dir  17618  mulgdir  17620  mulgass  17626  mulgnn0di  18277  mulgdi  18278  dprd2da  18487  lmodprop2d  18973  lssintcl  19012  prdslmodd  19017  islmhm2  19086  islbs2  19202  islbs3  19203  dmatmul  20351  mdetmul  20477  restopnb  21027  iunconn  21279  1stcelcls  21312  blsscls2  22356  stdbdbl  22369  xrsblre  22661  icccmplem2  22673  itg1val2  23496  cvxcl  24756  colline  25589  tglowdim2ln  25591  f1otrg  25796  f1otrge  25797  ax5seglem4  25857  ax5seglem5  25858  axcontlem3  25891  axcontlem8  25896  axcontlem9  25897  eengtrkg  25910  frgr3v  27255  xrofsup  29661  submomnd  29838  ogrpaddltbi  29847  erdszelem8  31306  resconn  31354  cvmliftmolem2  31390  cvmlift2lem12  31422  conway  32035  broutsideof3  32358  outsideoftr  32361  outsidele  32364  ltltncvr  35027  atcvrj2b  35036  cvrat4  35047  cvrat42  35048  2at0mat0  35129  islpln2a  35152  paddasslem11  35434  pmod1i  35452  lhpm0atN  35633  lautcvr  35696  cdlemg4c  36217  tendoplass  36388  tendodi1  36389  tendodi2  36390  dgrsub2  38022  ssinc  39578  ssdec  39579  ioondisj2  40032  ioondisj1  40033  pfxccat3  41751  ply1mulgsumlem2  42500
  Copyright terms: Public domain W3C validator