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

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

Proof of Theorem simprrl
StepHypRef Expression
1 simpl 486 . 2 ((𝜒𝜃) → 𝜒)
21ad2antll 728 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  prproe  4801  f1prex  7022  wfrlem17  7958  eroveu  8379  undom  8592  mapdom2  8676  domunfican  8779  fofinf1o  8787  finsschain  8819  wemaplem3  9000  oemapvali  9135  iunfictbso  9529  enfin2i  9736  fin1a2s  9829  ttukeylem6  9929  distrlem4pr  10441  mulcmpblnr  10486  prsrlem1  10487  dedekind  10796  divdivdiv  11334  divmuleq  11338  divsubdiv  11349  lediv12a  11526  xralrple  12590  ssfzo12bi  13131  seqcaopr  13407  leexp2r  13538  hashbclem  13810  wrd2ind  14080  rtrclreclem3  14415  rtrclreclem4  14416  relexpindlem  14418  rtrclind  14420  rlimresb  14918  summo  15070  fsum2dlem  15121  prodmo  15286  fprod2dlem  15330  bezoutlem3  15883  bezoutlem4  15884  ncoprmgcdne1b  15988  qredeu  15996  coprmproddvdslem  16000  pcqmul  16184  pcadd  16219  pockthg  16236  prmreclem2  16247  vdwlem10  16320  ramub1lem2  16357  prmgaplem6  16386  prmgaplem7  16387  cshwsdisj  16428  mreexexlem4d  16914  mreexdomd  16916  issubc3  17115  cofucl  17154  setcmon  17343  setcepi  17344  drsdirfi  17544  poslubmo  17752  posglbmo  17753  grpridd  17881  issubmd  17967  mndind  17988  ghmpreima  18376  gaorber  18434  psgnunilem4  18621  psgneu  18630  odcau  18725  pgpssslw  18735  fislw  18746  lsmsubm  18774  efgsfo  18861  gsum2d2  19091  pgpfac1lem5  19198  pgpfac1  19199  pgpfaclem2  19201  pgpfaclem3  19202  unitgrp  19417  lmodprop2d  19693  lsspropd  19786  lbsextlem4  19930  assapropd  20562  evlslem1  20758  mdetunilem8  21228  mdetuni0  21230  mdetmul  21232  neiint  21713  restbas  21767  iscnp4  21872  cnpco  21876  nrmsep  21966  regsep2  21985  ordthauslem  21992  1stcfb  22054  1stcrest  22062  2ndcctbss  22064  2ndcdisj  22065  2ndcomap  22067  dis2ndc  22069  nlly2i  22085  islly2  22093  hausllycmp  22103  lly1stc  22105  comppfsc  22141  ptbasin  22186  txcls  22213  ptcnp  22231  txlly  22245  txnlly  22246  txtube  22249  txcmplem1  22250  txcmplem2  22251  xkococnlem  22268  basqtop  22320  regr1lem  22348  kqreglem1  22350  kqreglem2  22351  kqnrmlem1  22352  kqnrmlem2  22353  reghmph  22402  nrmhmph  22403  opnfbas  22451  rnelfmlem  22561  fmufil  22568  fclscf  22634  fclsfnflim  22636  flimfnfcls  22637  uffclsflim  22640  cnpfcfi  22649  cnpfcf  22650  alexsubALTlem2  22657  alexsubALTlem4  22659  tgpconncompeqg  22721  ghmcnp  22724  qustgplem  22730  tsmsxp  22764  blssps  23035  blss  23036  blcld  23116  metequiv2  23121  met2ndci  23133  prdsxmslem2  23140  txmetcnp  23158  nlmvscnlem1  23296  xrge0tsms  23443  ipcnlem1  23853  iscmet3  23901  metsscmetcld  23923  minveclem3  24037  pmltpc  24058  ovolscalem2  24122  ovolicc2lem5  24129  ovolicc2  24130  nulmbl2  24144  ioombl1  24170  uniioombllem6  24196  uniioombl  24197  vitalilem3  24218  i1faddlem  24301  mbfmullem  24333  itg2split  24357  lhop2  24622  dvfsumrlim  24638  itgsubst  24656  plydivex  24897  plyexmo  24913  ulmbdd  24997  cxploglim  25567  dchrptlem2  25853  lgsquad2lem2  25973  2sqlem5  26010  dchrvmasumif  26091  rpvmasum2  26100  dchrisum0re  26101  dchrisum0lem3  26107  dchrisum0  26108  dchrmusum  26112  dchrvmasum  26113  pntibndlem3  26180  pntlemp  26198  ostth3  26226  legtrid  26389  hlcgreu  26416  mirreu3  26452  midexlem  26490  opphllem  26533  mideulem  26534  opphllem1  26545  oppperpex  26551  lnperpex  26601  trgcopy  26602  iscgra1  26608  cgraswap  26618  cgracom  26620  cgratr  26621  flatcgra  26622  acopyeu  26632  ax5seglem9  26735  ax5seg  26736  axcontlem8  26769  axcontlem12  26773  clwwlknonwwlknonb  27895  2pthfrgr  28073  frgrnbnb  28082  ablo4  28337  smcnlem  28484  pjhthmo  29089  mdslmd1lem1  30112  xrge0tsmsd  30746  locfinref  31198  xpinpreima2  31264  qqhval2  31337  dya2iocnrect  31653  orvcgteel  31839  orvclteel  31844  derangenlem  32532  cnpconn  32591  txpconn  32593  connpconn  32596  pconnpi1  32598  iccllysconn  32611  rellysconn  32612  cvmcov2  32636  cvmliftmolem2  32643  cvmliftmo  32645  cvmliftlem15  32659  cvmliftpht  32679  cvmlift3lem2  32681  fpr3g  33236  nosupbnd1lem1  33322  nosupbnd2  33330  conway  33378  cgrextend  33583  btwnouttr2  33597  cgrsub  33620  cgrxfr  33630  btwnxfr  33631  colineardim1  33636  btwnconn1lem6  33667  btwnconn1lem13  33674  btwnconn1lem14  33675  btwnconn3  33678  seglecgr12im  33685  segleantisym  33690  outsideofeq  33705  outsidele  33707  lineunray  33722  linethru  33728  fnessref  33819  neibastop2lem  33822  neibastop2  33823  unblimceq0lem  33959  knoppndvlem22  33986  bj-finsumval0  34701  isbasisrelowllem1  34773  isbasisrelowllem2  34774  mblfinlem3  35095  cnambfre  35104  areacirclem5  35148  istotbnd3  35208  sstotbnd  35212  crngm4  35440  cvlcvr1  36634  4atlem12  36907  paddasslem10  37124  paddasslem12  37126  paddasslem13  37127  lhpexle3lem  37306  cdlemd4  37496  cdleme0cq  37510  cdlemefs32sn1aw  37709  cdleme43fsv1snlem  37715  cdleme32d  37739  cdleme32f  37741  cdleme40m  37762  cdleme40n  37763  cdleme42keg  37781  cdleme42mgN  37783  cdleme50trn2  37846  cdleme50trn3  37848  cdlemm10N  38413  dihvalcqpre  38530  dihopelvalcpre  38543  dihmeetlem1N  38585  dihjat1lem  38723  mapd0  38960  mapdh9a  39084  fsuppssind  39456  diophin  39710  pellexlem3  39769  pellexlem5  39771  pellex  39773  pell14qrmulcl  39801  jm2.19lem3  39929  jm2.25  39937  jm2.27b  39944  lmhmfgsplit  40027  hbtlem2  40065  hbtlem5  40069  gsumws3  40899  gsumws4  40900  mnuprdlem4  40980  fnchoice  41655  stoweidlem17  42656  stoweidlem53  42692  stoweidlem61  42700  qndenserrnbllem  42933  bgoldbtbnd  44324  rabsubmgmd  44408  lindslinindsimp1  44863
  Copyright terms: Public domain W3C validator