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

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

Proof of Theorem simprrr
StepHypRef Expression
1 simpr 473 . 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  4628  f1prex  6763  fliftfun  6786  grpridd  7104  wfrlem17  7667  mapdom2  8370  domunfican  8472  fofinf1o  8480  finsschain  8512  wemaplem3  8692  oemapvali  8828  iunfictbso  9220  enfin2i  9428  fin1a2s  9521  distrlem4pr  10133  mulcmpblnr  10177  prsrlem1  10178  addsrmo  10179  mulsrmo  10180  divdivdiv  11011  divsubdiv  11026  lediv12a  11201  xralrple  12254  seqcaopr  13061  leexp2r  13141  hashbclem  13453  wrd2ind  13701  cshwidxmod  13773  rtrclreclem4  14024  relexpindlem  14026  rtrclind  14028  rlimresb  14519  summo  14671  fsum2dlem  14724  prodmo  14887  fprod2dlem  14931  bezoutlem3  15477  bezoutlem4  15478  qredeu  15590  coprmproddvdslem  15594  pcqmul  15775  pcadd  15810  pockthg  15827  ramub1lem2  15948  cshwsdisj  16017  mreexexlem4d  16512  issubc3  16713  cofucl  16752  setcmon  16941  setcepi  16942  drsdirfi  17143  poslubmo  17351  posglbmo  17352  ghmpreima  17884  gaorber  17942  psgnunilem4  18118  psgneu  18127  odcau  18220  pgpssslw  18230  fislw  18241  lsmsubm  18269  efgsfo  18353  pgpfac1  18681  pgpfaclem2  18683  pgpfaclem3  18684  unitgrp  18869  islmodd  19073  lmodprop2d  19129  lsspropd  19224  lbsextlem4  19370  assapropd  19536  evlslem1  19723  mdetunilem8  20636  mdetmul  20640  ppttop  21025  epttop  21027  restbas  21176  iscnp4  21281  cnpco  21285  nrmsep  21375  regsep2  21394  ordthauslem  21401  1stcfb  21462  2ndcctbss  21472  2ndcdisj  21473  2ndcomap  21475  dis2ndc  21477  1stcelcls  21478  nlly2i  21493  islly2  21501  hausllycmp  21511  lly1stc  21513  comppfsc  21549  1stckgenlem  21570  ptbasin  21594  txcls  21621  ptcnp  21639  txlly  21653  txnlly  21654  txtube  21657  txcmplem1  21658  txcmplem2  21659  xkococnlem  21676  basqtop  21728  regr1lem  21756  kqreglem1  21758  kqreglem2  21759  kqnrmlem1  21760  kqnrmlem2  21761  reghmph  21810  nrmhmph  21811  filuni  21902  rnelfmlem  21969  fmufil  21976  fclscf  22042  fclsfnflim  22044  flimfnfcls  22045  uffclsflim  22048  cnpfcfi  22057  cnpfcf  22058  alexsublem  22061  alexsubALTlem3  22066  tgpconncompeqg  22128  ghmcnp  22131  qustgplem  22137  blssps  22442  blss  22443  blcld  22523  metequiv2  22528  met2ndci  22540  prdsxmslem2  22547  txmetcnp  22565  nlmvscnlem1  22703  xrge0tsms  22850  ipcnlem1  23256  iscmet3  23303  cmetss  23325  minveclem3  23412  pmltpc  23431  ovolscalem2  23495  ovolicc2lem5  23502  ovolicc2  23503  nulmbl2  23517  ioombl1  23543  uniioombllem6  23569  uniioombl  23570  vitalilem3  23591  i1faddlem  23674  mbfmullem  23706  itg2const2  23722  itg2split  23730  lhop2  23992  dvfsumrlim  24008  itgsubst  24026  plydivex  24266  plyexmo  24282  ulmbdd  24366  cxploglim  24918  dchrptlem2  25204  lgsquad2lem2  25324  2sqlem5  25361  dchrvmasumif  25406  rpvmasum2  25415  dchrisum0re  25416  dchrisum0lem3  25422  dchrisum0  25423  dchrmusum  25427  dchrvmasum  25428  pntibndlem3  25495  pntlemp  25513  ostth3  25541  legtrid  25700  hlcgreu  25727  mirreu3  25763  opphllem  25841  oppperpex  25859  lnperpex  25909  trgcopy  25910  iscgra1  25916  cgraswap  25926  cgracom  25928  cgratr  25929  acopyeu  25939  ax5seglem9  26031  ax5seg  26032  axcontlem8  26065  axcontlem12  26069  upgrclwlkcompim  26905  wlkwwlkfunOLD  27023  wwlksnextwrd  27034  2pthfrgr  27459  frgrnbnb  27468  ablo4  27733  smcnlem  27880  pjhthmo  28489  1stpreimas  29810  xrge0tsmsd  30110  locfinref  30233  xpinpreima2  30278  qqhval2  30351  dya2iocnrect  30668  orvcgteel  30854  orvclteel  30859  cnpconn  31535  txpconn  31537  connpconn  31540  pconnpi1  31542  iccllysconn  31555  rellysconn  31556  cvmcov2  31580  cvmliftmolem2  31587  cvmliftmo  31589  cvmliftlem15  31603  cvmliftpht  31623  cvmlift3lem2  31625  nosupbnd1lem1  32175  nosupbnd2  32183  conway  32231  cgrextend  32436  btwnouttr2  32450  btwnexch2  32451  cgrxfr  32483  lineext  32504  btwnconn1lem5  32519  btwnconn1lem13  32527  btwnconn3  32531  segletr  32542  segleantisym  32543  outsideofeq  32558  outsidele  32560  lineunray  32575  refssfne  32674  neibastop2lem  32676  neibastop2  32677  unblimceq0lem  32814  knoppndvlem22  32841  mblfinlem3  33761  mblfinlem4  33762  cnambfre  33770  itg2addnclem  33773  areacirclem5  33816  istotbnd3  33881  crngm4  34113  cvlcvr1  35119  4atlem12  35392  cdlemb  35574  paddasslem10  35609  paddasslem12  35611  paddasslem13  35612  lhpexle3lem  35791  cdlemd4  35982  cdlemefs32sn1aw  36195  cdleme43fsv1snlem  36201  cdleme32d  36225  cdleme32f  36227  cdleme40m  36248  cdleme40n  36249  cdleme50trn2  36332  cdlemftr3  36346  cdlemm10N  36899  dihvalcqpre  37016  dihopelvalcpre  37029  dihmeetlem1N  37071  dihglblem5apreN  37072  dihmeetlem4preN  37087  dihjat1lem  37209  mapd0  37446  mapdh9a  37570  mzpmfp  37812  mzpcompact2lem  37816  diophin  37838  pellexlem3  37897  pellex  37901  pell14qrmulcl  37929  jm2.19lem3  38059  jm2.25  38067  jm2.27b  38074  fnwe2lem2  38122  hbtlem2  38195  hbtlem5  38199  gsumws3  38999  gsumws4  39000  fnchoice  39682  stoweidlem53  40749  stoweidlem61  40757  qndenserrnbllem  40993  bgoldbtbnd  42272
  Copyright terms: Public domain W3C validator