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

Theorem simprrl 790
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simprrl ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) → 𝜒)

Proof of Theorem simprrl
StepHypRef Expression
1 simpl 470 . 2 ((𝜒𝜃) → 𝜒)
21ad2antll 711 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  prproe  4621  f1prex  6757  grpridd  7098  wfrlem17  7661  eroveu  8072  undom  8281  mapdom2  8364  domunfican  8466  fofinf1o  8474  finsschain  8506  wemaplem3  8686  oemapvali  8822  iunfictbso  9214  enfin2i  9422  fin1a2s  9515  ttukeylem6  9615  distrlem4pr  10127  mulcmpblnr  10171  prsrlem1  10172  dedekind  10479  divdivdiv  11005  divmuleq  11009  divsubdiv  11020  lediv12a  11195  xralrple  12248  ssfzo12bi  12781  seqcaopr  13055  leexp2r  13135  hashbclem  13447  wrd2ind  13695  rtrclreclem3  14017  rtrclreclem4  14018  relexpindlem  14020  rtrclind  14022  rlimresb  14513  summo  14665  fsum2dlem  14718  prodmo  14881  fprod2dlem  14925  bezoutlem3  15471  bezoutlem4  15472  ncoprmgcdne1b  15576  qredeu  15584  coprmproddvdslem  15588  pcqmul  15769  pcadd  15804  pockthg  15821  prmreclem2  15832  vdwlem10  15905  ramub1lem2  15942  prmgaplem6  15971  prmgaplem7  15972  cshwsdisj  16011  mreexexlem4d  16506  mreexdomd  16508  issubc3  16707  cofucl  16746  setcmon  16935  setcepi  16936  drsdirfi  17137  poslubmo  17345  posglbmo  17346  issubmd  17548  mrcmndind  17565  ghmpreima  17878  gaorber  17936  psgnunilem4  18112  psgneu  18121  odcau  18214  pgpssslw  18224  fislw  18235  lsmsubm  18263  efgsfo  18347  gsum2d2  18568  pgpfac1lem5  18674  pgpfac1  18675  pgpfaclem2  18677  pgpfaclem3  18678  unitgrp  18863  lmodprop2d  19123  lsspropd  19218  lbsextlem4  19364  assapropd  19530  evlslem1  19717  mdetunilem8  20630  mdetuni0  20632  mdetmul  20634  neiint  21116  restbas  21170  iscnp4  21275  cnpco  21279  nrmsep  21369  regsep2  21388  ordthauslem  21395  1stcfb  21456  1stcrest  21464  2ndcctbss  21466  2ndcdisj  21467  2ndcomap  21469  dis2ndc  21471  nlly2i  21487  islly2  21495  hausllycmp  21505  lly1stc  21507  comppfsc  21543  ptbasin  21588  txcls  21615  ptcnp  21633  txlly  21647  txnlly  21648  txtube  21651  txcmplem1  21652  txcmplem2  21653  xkococnlem  21670  basqtop  21722  regr1lem  21750  kqreglem1  21752  kqreglem2  21753  kqnrmlem1  21754  kqnrmlem2  21755  reghmph  21804  nrmhmph  21805  opnfbas  21853  rnelfmlem  21963  fmufil  21970  fclscf  22036  fclsfnflim  22038  flimfnfcls  22039  uffclsflim  22042  cnpfcfi  22051  cnpfcf  22052  alexsubALTlem2  22059  alexsubALTlem4  22061  tgpconncompeqg  22122  ghmcnp  22125  qustgplem  22131  tsmsxp  22165  blssps  22436  blss  22437  blcld  22517  metequiv2  22522  met2ndci  22534  prdsxmslem2  22541  txmetcnp  22559  nlmvscnlem1  22697  xrge0tsms  22844  ipcnlem1  23250  iscmet3  23297  cmetss  23319  minveclem3  23406  pmltpc  23425  ovolscalem2  23489  ovolicc2lem5  23496  ovolicc2  23497  nulmbl2  23511  ioombl1  23537  uniioombllem6  23563  uniioombl  23564  vitalilem3  23585  i1faddlem  23668  mbfmullem  23700  itg2split  23724  lhop2  23986  dvfsumrlim  24002  itgsubst  24020  plydivex  24260  plyexmo  24276  ulmbdd  24360  cxploglim  24912  dchrptlem2  25198  lgsquad2lem2  25318  2sqlem5  25355  dchrvmasumif  25400  rpvmasum2  25409  dchrisum0re  25410  dchrisum0lem3  25416  dchrisum0  25417  dchrmusum  25421  dchrvmasum  25422  pntibndlem3  25489  pntlemp  25507  ostth3  25535  legtrid  25694  hlcgreu  25721  mirreu3  25757  midexlem  25795  opphllem  25835  mideulem  25836  opphllem1  25847  oppperpex  25853  lnperpex  25903  trgcopy  25904  iscgra1  25910  cgraswap  25920  cgracom  25922  cgratr  25923  acopyeu  25933  ax5seglem9  26025  ax5seg  26026  axcontlem8  26059  axcontlem12  26063  clwwlknonwwlknonb  27268  2pthfrgr  27453  frgrnbnb  27462  ablo4  27727  smcnlem  27874  pjhthmo  28483  mdslmd1lem1  29506  xrge0tsmsd  30104  locfinref  30227  xpinpreima2  30272  qqhval2  30345  dya2iocnrect  30662  orvcgteel  30848  orvclteel  30853  derangenlem  31470  cnpconn  31529  txpconn  31531  connpconn  31534  pconnpi1  31536  iccllysconn  31549  rellysconn  31550  cvmcov2  31574  cvmliftmolem2  31581  cvmliftmo  31583  cvmliftlem15  31597  cvmliftpht  31617  cvmlift3lem2  31619  nosupbnd1lem1  32169  nosupbnd2  32177  conway  32225  cgrextend  32430  btwnouttr2  32444  cgrsub  32467  cgrxfr  32477  btwnxfr  32478  colineardim1  32483  btwnconn1lem6  32514  btwnconn1lem13  32521  btwnconn1lem14  32522  btwnconn3  32525  seglecgr12im  32532  segleantisym  32537  outsideofeq  32552  outsidele  32554  lineunray  32569  linethru  32575  fnessref  32667  neibastop2lem  32670  neibastop2  32671  unblimceq0lem  32808  knoppndvlem22  32835  bj-finsumval0  33458  isbasisrelowllem1  33513  isbasisrelowllem2  33514  mblfinlem3  33755  cnambfre  33764  areacirclem5  33810  istotbnd3  33875  sstotbnd  33879  crngm4  34107  cvlcvr1  35113  4atlem12  35386  paddasslem10  35603  paddasslem12  35605  paddasslem13  35606  lhpexle3lem  35785  cdlemd4  35976  cdleme0cq  35990  cdlemefs32sn1aw  36189  cdleme43fsv1snlem  36195  cdleme32d  36219  cdleme32f  36221  cdleme40m  36242  cdleme40n  36243  cdleme42keg  36261  cdleme42mgN  36263  cdleme50trn2  36326  cdleme50trn3  36328  cdlemm10N  36893  dihvalcqpre  37010  dihopelvalcpre  37023  dihmeetlem1N  37065  dihjat1lem  37203  mapd0  37440  mapdh9a  37564  diophin  37832  pellexlem3  37891  pellexlem5  37893  pellex  37895  pell14qrmulcl  37923  jm2.19lem3  38053  jm2.25  38061  jm2.27b  38068  lmhmfgsplit  38151  hbtlem2  38189  hbtlem5  38193  gsumws3  38993  gsumws4  38994  fnchoice  39676  stoweidlem17  40707  stoweidlem53  40743  stoweidlem61  40751  qndenserrnbllem  40987  bgoldbtbnd  42266  rabsubmgmd  42353  lindslinindsimp1  42808
  Copyright terms: Public domain W3C validator