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

Theorem simplr3 1198
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simplr3 (((𝜃 ∧ (𝜑𝜓𝜒)) ∧ 𝜏) → 𝜒)

Proof of Theorem simplr3
StepHypRef Expression
1 simp3 1119 . 2 ((𝜑𝜓𝜒) → 𝜒)
21ad2antlr 715 1 (((𝜃 ∧ (𝜑𝜓𝜒)) ∧ 𝜏) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  w3a 1069
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 199  df-an 388  df-3an 1071
This theorem is referenced by:  soltmin  5833  frfi  8556  wemappo  8806  iccsplit  12685  ccatswrd  13847  pfxccat3  13934  swrdccat3OLD  13935  modfsummods  15006  pcdvdstr  16066  vdwlem12  16182  cshwsidrepswmod0  16282  iscatd2  16822  oppccomfpropd  16867  initoeu2lem0  17143  resssetc  17222  resscatc  17235  yonedalem4c  17397  mod1ile  17585  mod2ile  17586  prdsmndd  17803  grprcan  17936  mulgnn0dir  18053  mulgdir  18055  mulgass  18060  mulgnn0di  18716  mulgdi  18717  dprd2da  18926  lmodprop2d  19430  lssintcl  19470  prdslmodd  19475  islmhm2  19544  islbs2  19660  islbs3  19661  dmatmul  20825  mdetmul  20951  restopnb  21502  iunconn  21755  1stcelcls  21788  blsscls2  22832  stdbdbl  22845  xrsblre  23137  icccmplem2  23149  itg1val2  24003  cvxcl  25279  colline  26152  tglowdim2ln  26154  f1otrg  26375  f1otrge  26376  ax5seglem4  26436  ax5seglem5  26437  axcontlem3  26470  axcontlem8  26475  axcontlem9  26476  eengtrkg  26490  frgr3v  27824  xrofsup  30268  submomnd  30455  ogrpaddltbi  30464  erdszelem8  32067  resconn  32115  cvmliftmolem2  32151  cvmlift2lem12  32183  conway  32822  broutsideof3  33145  outsideoftr  33148  outsidele  33151  ltltncvr  36041  atcvrj2b  36050  cvrat4  36061  cvrat42  36062  2at0mat0  36143  islpln2a  36166  paddasslem11  36448  pmod1i  36466  lhpm0atN  36647  lautcvr  36710  cdlemg4c  37230  tendoplass  37401  tendodi1  37402  tendodi2  37403  dgrsub2  39169  grumnud  40035  ssinc  40809  ssdec  40810  ioondisj2  41230  ioondisj1  41231  ply1mulgsumlem2  43840
  Copyright terms: Public domain W3C validator