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

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

Proof of Theorem simprrl
StepHypRef Expression
1 simpl 483 . 2 ((𝜒𝜃) → 𝜒)
21ad2antll 725 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  prproe  4830  f1prex  7031  wfrlem17  7962  eroveu  8382  undom  8594  mapdom2  8677  domunfican  8780  fofinf1o  8788  finsschain  8820  wemaplem3  9001  oemapvali  9136  iunfictbso  9529  enfin2i  9732  fin1a2s  9825  ttukeylem6  9925  distrlem4pr  10437  mulcmpblnr  10482  prsrlem1  10483  dedekind  10792  divdivdiv  11330  divmuleq  11334  divsubdiv  11345  lediv12a  11522  xralrple  12588  ssfzo12bi  13122  seqcaopr  13397  leexp2r  13528  hashbclem  13800  wrd2ind  14075  rtrclreclem3  14409  rtrclreclem4  14410  relexpindlem  14412  rtrclind  14414  rlimresb  14912  summo  15064  fsum2dlem  15115  prodmo  15280  fprod2dlem  15324  bezoutlem3  15879  bezoutlem4  15880  ncoprmgcdne1b  15984  qredeu  15992  coprmproddvdslem  15996  pcqmul  16180  pcadd  16215  pockthg  16232  prmreclem2  16243  vdwlem10  16316  ramub1lem2  16353  prmgaplem6  16382  prmgaplem7  16383  cshwsdisj  16422  mreexexlem4d  16908  mreexdomd  16910  issubc3  17109  cofucl  17148  setcmon  17337  setcepi  17338  drsdirfi  17538  poslubmo  17746  posglbmo  17747  grpridd  17875  issubmd  17961  mndind  17982  ghmpreima  18320  gaorber  18378  psgnunilem4  18556  psgneu  18565  odcau  18660  pgpssslw  18670  fislw  18681  lsmsubm  18709  efgsfo  18796  gsum2d2  19025  pgpfac1lem5  19132  pgpfac1  19133  pgpfaclem2  19135  pgpfaclem3  19136  unitgrp  19348  lmodprop2d  19627  lsspropd  19720  lbsextlem4  19864  assapropd  20031  evlslem1  20225  mdetunilem8  21158  mdetuni0  21160  mdetmul  21162  neiint  21642  restbas  21696  iscnp4  21801  cnpco  21805  nrmsep  21895  regsep2  21914  ordthauslem  21921  1stcfb  21983  1stcrest  21991  2ndcctbss  21993  2ndcdisj  21994  2ndcomap  21996  dis2ndc  21998  nlly2i  22014  islly2  22022  hausllycmp  22032  lly1stc  22034  comppfsc  22070  ptbasin  22115  txcls  22142  ptcnp  22160  txlly  22174  txnlly  22175  txtube  22178  txcmplem1  22179  txcmplem2  22180  xkococnlem  22197  basqtop  22249  regr1lem  22277  kqreglem1  22279  kqreglem2  22280  kqnrmlem1  22281  kqnrmlem2  22282  reghmph  22331  nrmhmph  22332  opnfbas  22380  rnelfmlem  22490  fmufil  22497  fclscf  22563  fclsfnflim  22565  flimfnfcls  22566  uffclsflim  22569  cnpfcfi  22578  cnpfcf  22579  alexsubALTlem2  22586  alexsubALTlem4  22588  tgpconncompeqg  22649  ghmcnp  22652  qustgplem  22658  tsmsxp  22692  blssps  22963  blss  22964  blcld  23044  metequiv2  23049  met2ndci  23061  prdsxmslem2  23068  txmetcnp  23086  nlmvscnlem1  23224  xrge0tsms  23371  ipcnlem1  23777  iscmet3  23825  metsscmetcld  23847  minveclem3  23961  pmltpc  23980  ovolscalem2  24044  ovolicc2lem5  24051  ovolicc2  24052  nulmbl2  24066  ioombl1  24092  uniioombllem6  24118  uniioombl  24119  vitalilem3  24140  i1faddlem  24223  mbfmullem  24255  itg2split  24279  lhop2  24541  dvfsumrlim  24557  itgsubst  24575  plydivex  24815  plyexmo  24831  ulmbdd  24915  cxploglim  25483  dchrptlem2  25769  lgsquad2lem2  25889  2sqlem5  25926  dchrvmasumif  26007  rpvmasum2  26016  dchrisum0re  26017  dchrisum0lem3  26023  dchrisum0  26024  dchrmusum  26028  dchrvmasum  26029  pntibndlem3  26096  pntlemp  26114  ostth3  26142  legtrid  26305  hlcgreu  26332  mirreu3  26368  midexlem  26406  opphllem  26449  mideulem  26450  opphllem1  26461  oppperpex  26467  lnperpex  26517  trgcopy  26518  iscgra1  26524  cgraswap  26534  cgracom  26536  cgratr  26537  flatcgra  26538  acopyeu  26548  ax5seglem9  26651  ax5seg  26652  axcontlem8  26685  axcontlem12  26689  clwwlknonwwlknonb  27813  2pthfrgr  27991  frgrnbnb  28000  ablo4  28255  smcnlem  28402  pjhthmo  29007  mdslmd1lem1  30030  xrge0tsmsd  30620  locfinref  31005  xpinpreima2  31050  qqhval2  31123  dya2iocnrect  31439  orvcgteel  31625  orvclteel  31630  derangenlem  32316  cnpconn  32375  txpconn  32377  connpconn  32380  pconnpi1  32382  iccllysconn  32395  rellysconn  32396  cvmcov2  32420  cvmliftmolem2  32427  cvmliftmo  32429  cvmliftlem15  32443  cvmliftpht  32463  cvmlift3lem2  32465  fpr3g  33020  nosupbnd1lem1  33106  nosupbnd2  33114  conway  33162  cgrextend  33367  btwnouttr2  33381  cgrsub  33404  cgrxfr  33414  btwnxfr  33415  colineardim1  33420  btwnconn1lem6  33451  btwnconn1lem13  33458  btwnconn1lem14  33459  btwnconn3  33462  seglecgr12im  33469  segleantisym  33474  outsideofeq  33489  outsidele  33491  lineunray  33506  linethru  33512  fnessref  33603  neibastop2lem  33606  neibastop2  33607  unblimceq0lem  33743  knoppndvlem22  33770  bj-finsumval0  34456  isbasisrelowllem1  34519  isbasisrelowllem2  34520  mblfinlem3  34813  cnambfre  34822  areacirclem5  34868  istotbnd3  34932  sstotbnd  34936  crngm4  35164  cvlcvr1  36357  4atlem12  36630  paddasslem10  36847  paddasslem12  36849  paddasslem13  36850  lhpexle3lem  37029  cdlemd4  37219  cdleme0cq  37233  cdlemefs32sn1aw  37432  cdleme43fsv1snlem  37438  cdleme32d  37462  cdleme32f  37464  cdleme40m  37485  cdleme40n  37486  cdleme42keg  37504  cdleme42mgN  37506  cdleme50trn2  37569  cdleme50trn3  37571  cdlemm10N  38136  dihvalcqpre  38253  dihopelvalcpre  38266  dihmeetlem1N  38308  dihjat1lem  38446  mapd0  38683  mapdh9a  38807  diophin  39249  pellexlem3  39308  pellexlem5  39310  pellex  39312  pell14qrmulcl  39340  jm2.19lem3  39468  jm2.25  39476  jm2.27b  39483  lmhmfgsplit  39566  hbtlem2  39604  hbtlem5  39608  gsumws3  40430  gsumws4  40431  mnuprdlem4  40491  fnchoice  41166  stoweidlem17  42183  stoweidlem53  42219  stoweidlem61  42227  qndenserrnbllem  42460  bgoldbtbnd  43821  rabsubmgmd  43905  lindslinindsimp1  44410
  Copyright terms: Public domain W3C validator