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

Theorem simprrl 821
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 765 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 197  df-an 385
This theorem is referenced by:  prproe  4466  f1prex  6579  grpridd  6916  wfrlem17  7476  eroveu  7885  undom  8089  mapdom2  8172  domunfican  8274  fofinf1o  8282  finsschain  8314  wemaplem3  8494  oemapvali  8619  iunfictbso  8975  enfin2i  9181  fin1a2s  9274  ttukeylem6  9374  distrlem4pr  9886  mulcmpblnr  9930  prsrlem1  9931  dedekind  10238  divdivdiv  10764  divmuleq  10768  divsubdiv  10779  lediv12a  10954  xralrple  12074  ssfzo12bi  12603  seqcaopr  12878  leexp2r  12958  hashbclem  13274  wrd2ind  13523  rtrclreclem3  13844  rtrclreclem4  13845  relexpindlem  13847  rtrclind  13849  rlimresb  14340  summo  14492  fsum2dlem  14545  prodmo  14710  fprod2dlem  14754  bezoutlem3  15305  bezoutlem4  15306  ncoprmgcdne1b  15410  qredeu  15419  coprmproddvdslem  15423  pcqmul  15605  pcadd  15640  pockthg  15657  prmreclem2  15668  vdwlem10  15741  ramub1lem2  15778  prmgaplem6  15807  prmgaplem7  15808  cshwsdisj  15852  mreexexlem4d  16354  mreexdomd  16357  issubc3  16556  cofucl  16595  setcmon  16784  setcepi  16785  drsdirfi  16985  poslubmo  17193  posglbmo  17194  issubmd  17396  mrcmndind  17413  ghmpreima  17729  gaorber  17787  psgnunilem4  17963  psgneu  17972  odcau  18065  pgpssslw  18075  fislw  18086  lsmsubm  18114  efgsfo  18198  gsum2d2  18419  pgpfac1lem5  18524  pgpfac1  18525  pgpfaclem2  18527  pgpfaclem3  18528  unitgrp  18713  lmodprop2d  18973  lsspropd  19065  lbsextlem4  19209  assapropd  19375  evlslem1  19563  mdetunilem8  20473  mdetuni0  20475  mdetmul  20477  neiint  20956  restbas  21010  iscnp4  21115  cnpco  21119  nrmsep  21209  regsep2  21228  ordthauslem  21235  1stcfb  21296  1stcrest  21304  2ndcctbss  21306  2ndcdisj  21307  2ndcomap  21309  dis2ndc  21311  nlly2i  21327  islly2  21335  hausllycmp  21345  lly1stc  21347  comppfsc  21383  ptbasin  21428  txcls  21455  ptcnp  21473  txlly  21487  txnlly  21488  txtube  21491  txcmplem1  21492  txcmplem2  21493  xkococnlem  21510  basqtop  21562  regr1lem  21590  kqreglem1  21592  kqreglem2  21593  kqnrmlem1  21594  kqnrmlem2  21595  reghmph  21644  nrmhmph  21645  opnfbas  21693  rnelfmlem  21803  fmufil  21810  fclscf  21876  fclsfnflim  21878  flimfnfcls  21879  uffclsflim  21882  cnpfcfi  21891  cnpfcf  21892  alexsubALTlem2  21899  alexsubALTlem4  21901  tgpconncompeqg  21962  ghmcnp  21965  qustgplem  21971  tsmsxp  22005  blssps  22276  blss  22277  blcld  22357  metequiv2  22362  met2ndci  22374  prdsxmslem2  22381  txmetcnp  22399  nlmvscnlem1  22537  xrge0tsms  22684  ipcnlem1  23090  iscmet3  23137  cmetss  23159  minveclem3  23246  pmltpc  23265  ovolscalem2  23328  ovolicc2lem5  23335  ovolicc2  23336  nulmbl2  23350  ioombl1  23376  uniioombllem6  23402  uniioombl  23403  vitalilem3  23424  i1faddlem  23505  mbfmullem  23537  itg2split  23561  lhop2  23823  dvfsumrlim  23839  itgsubst  23857  plydivex  24097  plyexmo  24113  ulmbdd  24197  cxploglim  24749  dchrptlem2  25035  lgsquad2lem2  25155  2sqlem5  25192  dchrvmasumif  25237  rpvmasum2  25246  dchrisum0re  25247  dchrisum0lem3  25253  dchrisum0  25254  dchrmusum  25258  dchrvmasum  25259  pntibndlem3  25326  pntlemp  25344  ostth3  25372  legtrid  25531  hlcgreu  25558  mirreu3  25594  midexlem  25632  opphllem  25672  mideulem  25673  opphllem1  25684  oppperpex  25690  lnperpex  25740  trgcopy  25741  iscgra1  25747  cgraswap  25757  cgracom  25759  cgratr  25760  acopyeu  25770  ax5seglem9  25862  ax5seg  25863  axcontlem8  25896  axcontlem12  25900  clwwlknonwwlknonb  27080  2pthfrgr  27264  frgrnbnb  27273  ablo4  27532  smcnlem  27680  pjhthmo  28289  mdslmd1lem1  29312  xrge0tsmsd  29913  locfinref  30036  xpinpreima2  30081  qqhval2  30154  dya2iocnrect  30471  orvcgteel  30657  orvclteel  30662  derangenlem  31279  cnpconn  31338  txpconn  31340  connpconn  31343  pconnpi1  31345  iccllysconn  31358  rellysconn  31359  cvmcov2  31383  cvmliftmolem2  31390  cvmliftmo  31392  cvmliftlem15  31406  cvmliftpht  31426  cvmlift3lem2  31428  nosupbnd1lem1  31979  nosupbnd2  31987  conway  32035  cgrextend  32240  btwnouttr2  32254  cgrsub  32277  cgrxfr  32287  btwnxfr  32288  colineardim1  32293  btwnconn1lem6  32324  btwnconn1lem13  32331  btwnconn1lem14  32332  btwnconn3  32335  seglecgr12im  32342  segleantisym  32347  outsideofeq  32362  outsidele  32364  lineunray  32379  linethru  32385  fnessref  32477  neibastop2lem  32480  neibastop2  32481  unblimceq0lem  32622  knoppndvlem22  32649  bj-finsumval0  33277  isbasisrelowllem1  33333  isbasisrelowllem2  33334  mblfinlem3  33578  cnambfre  33588  areacirclem5  33634  istotbnd3  33700  sstotbnd  33704  crngm4  33932  cvlcvr1  34944  4atlem12  35216  paddasslem10  35433  paddasslem12  35435  paddasslem13  35436  lhpexle3lem  35615  cdlemd4  35806  cdleme0cq  35820  cdlemefs32sn1aw  36019  cdleme43fsv1snlem  36025  cdleme32d  36049  cdleme32f  36051  cdleme40m  36072  cdleme40n  36073  cdleme42keg  36091  cdleme42mgN  36093  cdleme50trn2  36156  cdleme50trn3  36158  cdlemm10N  36724  dihvalcqpre  36841  dihopelvalcpre  36854  dihmeetlem1N  36896  dihjat1lem  37034  mapd0  37271  mapdh9a  37396  diophin  37653  pellexlem3  37712  pellexlem5  37714  pellex  37716  pell14qrmulcl  37744  jm2.19lem3  37875  jm2.25  37883  jm2.27b  37890  lmhmfgsplit  37973  hbtlem2  38011  hbtlem5  38015  gsumws3  38816  gsumws4  38817  fnchoice  39502  stoweidlem17  40552  stoweidlem53  40588  stoweidlem61  40596  qndenserrnbllem  40832  bgoldbtbnd  42022  rabsubmgmd  42116  lindslinindsimp1  42571
  Copyright terms: Public domain W3C validator