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

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

Proof of Theorem simplr3
StepHypRef Expression
1 simpr3 1067 . 2 ((𝜃 ∧ (𝜑𝜓𝜒)) → 𝜒)
21adantr 481 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:  soltmin  5495  frfi  8150  wemappo  8399  iccsplit  12244  ccatswrd  13389  swrdccat3  13424  pcdvdstr  15499  vdwlem12  15615  cshwsidrepswmod0  15720  iscatd2  16258  oppccomfpropd  16303  initoeu2lem0  16579  resssetc  16658  resscatc  16671  yonedalem4c  16833  mod1ile  17021  mod2ile  17022  prdsmndd  17239  grprcan  17371  mulgnn0dir  17487  mulgdir  17489  mulgass  17495  mulgnn0di  18147  mulgdi  18148  dprd2da  18357  lmodprop2d  18841  lssintcl  18878  prdslmodd  18883  islmhm2  18952  islbs2  19068  islbs3  19069  dmatmul  20217  mdetmul  20343  restopnb  20884  iunconn  21136  1stcelcls  21169  blsscls2  22214  stdbdbl  22227  xrsblre  22517  icccmplem2  22529  itg1val2  23352  cvxcl  24606  colline  25439  tglowdim2ln  25441  f1otrg  25646  f1otrge  25647  ax5seglem4  25707  ax5seglem5  25708  axcontlem3  25741  axcontlem8  25746  axcontlem9  25747  eengtrkg  25760  frgr3v  26997  xrofsup  29369  submomnd  29487  ogrpaddltbi  29496  erdszelem8  30880  resconn  30928  cvmliftmolem2  30964  cvmlift2lem12  30996  broutsideof3  31867  outsideoftr  31870  outsidele  31873  ltltncvr  34175  atcvrj2b  34184  cvrat4  34195  cvrat42  34196  2at0mat0  34277  islpln2a  34300  paddasslem11  34582  pmod1i  34600  lhpm0atN  34781  lautcvr  34844  cdlemg4c  35366  tendoplass  35537  tendodi1  35538  tendodi2  35539  dgrsub2  37172  ssinc  38735  ssdec  38736  ioondisj2  39112  ioondisj1  39113  pfxccat3  40713  ply1mulgsumlem2  41437
  Copyright terms: Public domain W3C validator