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

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

Proof of Theorem simprrl
StepHypRef Expression
1 simpl 472 . 2 ((𝜒𝜃) → 𝜒)
21ad2antll 761 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 196  df-an 385
This theorem is referenced by:  f1prex  6439  grpridd  6772  wfrlem17  7318  eroveu  7729  undom  7933  mapdom2  8016  domunfican  8118  fofinf1o  8126  finsschain  8156  wemaplem3  8336  oemapvali  8464  iunfictbso  8820  enfin2i  9026  fin1a2s  9119  ttukeylem6  9219  distrlem4pr  9727  mulcmpblnr  9771  prsrlem1  9772  dedekind  10079  divdivdiv  10605  divmuleq  10609  divsubdiv  10620  lediv12a  10795  xralrple  11910  ssfzo12bi  12429  seqcaopr  12700  leexp2r  12780  hashbclem  13093  wrd2ind  13329  rtrclreclem3  13648  rtrclreclem4  13649  relexpindlem  13651  rtrclind  13653  rlimresb  14144  summo  14295  fsum2dlem  14343  prodmo  14505  fprod2dlem  14549  bezoutlem3  15096  bezoutlem4  15097  ncoprmgcdne1b  15201  qredeu  15210  coprmproddvdslem  15214  pcqmul  15396  pcadd  15431  pockthg  15448  prmreclem2  15459  vdwlem10  15532  ramub1lem2  15569  prmgaplem6  15598  prmgaplem7  15599  cshwsdisj  15643  mreexexlem4d  16130  mreexdomd  16133  issubc3  16332  cofucl  16371  setcmon  16560  setcepi  16561  drsdirfi  16761  poslubmo  16969  posglbmo  16970  issubmd  17172  mrcmndind  17189  ghmpreima  17505  gaorber  17564  psgnunilem4  17740  psgneu  17749  odcau  17842  pgpssslw  17852  fislw  17863  lsmsubm  17891  efgsfo  17975  gsum2d2  18196  pgpfac1lem5  18301  pgpfac1  18302  pgpfaclem2  18304  pgpfaclem3  18305  unitgrp  18490  lmodprop2d  18748  lsspropd  18838  lbsextlem4  18982  assapropd  19148  evlslem1  19336  mdetunilem8  20244  mdetuni0  20246  mdetmul  20248  neiint  20718  restbas  20772  iscnp4  20877  cnpco  20881  nrmsep  20971  regsep2  20990  ordthauslem  20997  1stcfb  21058  1stcrest  21066  2ndcctbss  21068  2ndcdisj  21069  2ndcomap  21071  dis2ndc  21073  nlly2i  21089  islly2  21097  hausllycmp  21107  lly1stc  21109  comppfsc  21145  ptbasin  21190  txcls  21217  ptcnp  21235  txlly  21249  txnlly  21250  txtube  21253  txcmplem1  21254  txcmplem2  21255  xkococnlem  21272  basqtop  21324  regr1lem  21352  kqreglem1  21354  kqreglem2  21355  kqnrmlem1  21356  kqnrmlem2  21357  reghmph  21406  nrmhmph  21407  opnfbas  21456  rnelfmlem  21566  fmufil  21573  fclscf  21639  fclsfnflim  21641  flimfnfcls  21642  uffclsflim  21645  cnpfcfi  21654  cnpfcf  21655  alexsubALTlem2  21662  alexsubALTlem4  21664  tgpconcompeqg  21725  ghmcnp  21728  qustgplem  21734  tsmsxp  21768  blssps  22039  blss  22040  blcld  22120  metequiv2  22125  met2ndci  22137  prdsxmslem2  22144  txmetcnp  22162  nlmvscnlem1  22300  xrge0tsms  22445  ipcnlem1  22852  iscmet3  22899  cmetss  22921  minveclem3  23008  pmltpc  23026  ovolscalem2  23089  ovolicc2lem5  23096  ovolicc2  23097  nulmbl2  23111  ioombl1  23137  uniioombllem6  23162  uniioombl  23163  vitalilem3  23185  i1faddlem  23266  mbfmullem  23298  itg2split  23322  lhop2  23582  dvfsumrlim  23598  itgsubst  23616  plydivex  23856  plyexmo  23872  ulmbdd  23956  cxploglim  24504  dchrptlem2  24790  lgsquad2lem2  24910  2sqlem5  24947  dchrvmasumif  24992  rpvmasum2  25001  dchrisum0re  25002  dchrisum0lem3  25008  dchrisum0  25009  dchrmusum  25013  dchrvmasum  25014  pntibndlem3  25081  pntlemp  25099  ostth3  25127  legtrid  25286  hlcgreu  25313  mirreu3  25349  midexlem  25387  opphllem  25427  mideulem  25428  opphllem1  25439  oppperpex  25445  lnperpex  25495  trgcopy  25496  iscgra1  25502  cgraswap  25512  cgracom  25514  cgratr  25515  acopyeu  25525  ax5seglem9  25617  ax5seg  25618  axcontlem8  25651  axcontlem12  25655  cusgrafilem1  26007  2spotiundisj  26589  ablo4  26788  smcnlem  26936  pjhthmo  27545  mdslmd1lem1  28568  xrge0tsmsd  29116  locfinref  29236  xpinpreima2  29281  qqhval2  29354  dya2iocnrect  29670  orvcgteel  29856  orvclteel  29861  derangenlem  30407  cnpcon  30466  txpcon  30468  conpcon  30471  pconpi1  30473  iccllyscon  30486  rellyscon  30487  cvmcov2  30511  cvmliftmolem2  30518  cvmliftmo  30520  cvmliftlem15  30534  cvmliftpht  30554  cvmlift3lem2  30556  cgrextend  31285  btwnouttr2  31299  cgrsub  31322  cgrxfr  31332  btwnxfr  31333  colineardim1  31338  btwnconn1lem6  31369  btwnconn1lem13  31376  btwnconn1lem14  31377  btwnconn3  31380  seglecgr12im  31387  segleantisym  31392  outsideofeq  31407  outsidele  31409  lineunray  31424  linethru  31430  fnessref  31522  neibastop2lem  31525  neibastop2  31526  unblimceq0lem  31667  knoppndvlem22  31694  bj-finsumval0  32324  isbasisrelowllem1  32379  isbasisrelowllem2  32380  mblfinlem3  32618  cnambfre  32628  areacirclem5  32674  istotbnd3  32740  sstotbnd  32744  crngm4  32972  cvlcvr1  33644  4atlem12  33916  paddasslem10  34133  paddasslem12  34135  paddasslem13  34136  lhpexle3lem  34315  cdlemd4  34506  cdleme0cq  34520  cdlemefs32sn1aw  34720  cdleme43fsv1snlem  34726  cdleme32d  34750  cdleme32f  34752  cdleme40m  34773  cdleme40n  34774  cdleme42keg  34792  cdleme42mgN  34794  cdleme50trn2  34857  cdleme50trn3  34859  cdlemm10N  35425  dihvalcqpre  35542  dihopelvalcpre  35555  dihmeetlem1N  35597  dihjat1lem  35735  mapd0  35972  mapdh9a  36097  diophin  36354  pellexlem3  36413  pellexlem5  36415  pellex  36417  pell14qrmulcl  36445  jm2.19lem3  36576  jm2.25  36584  jm2.27b  36591  lmhmfgsplit  36674  hbtlem2  36713  hbtlem5  36717  gsumws3  37521  gsumws4  37522  fnchoice  38211  stoweidlem17  38910  stoweidlem53  38946  stoweidlem61  38954  qndenserrnbllem  39190  bgoldbtbnd  40225  2pthfrgr  41454  frgrnbnb  41463  rabsubmgmd  41581  lindslinindsimp1  42040
  Copyright terms: Public domain W3C validator