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

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

Proof of Theorem simplrr
StepHypRef Expression
1 simpr 476 . 2 ((𝜓𝜒) → 𝜒)
21ad2antlr 763 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:  disjxiun  4681  disjxiunOLD  4682  fsnex  6578  f1prex  6579  isotr  6626  weniso  6644  riota5f  6676  tfrlem9a  7527  oaass  7686  oeeui  7727  oaabs2  7770  resixpfo  7988  omxpenlem  8102  pw2f1olem  8105  fopwdom  8109  fofinf1o  8282  marypha1lem  8380  ordiso2  8461  oismo  8486  ixpiunwdom  8537  cantnf  8628  fseqenlem1  8885  iunfictbso  8975  dfac12lem2  9004  dfac12lem3  9005  infunsdom1  9073  infpssrlem5  9167  fin23lem24  9182  isf32lem2  9214  isf32lem4  9216  isf34lem4  9237  fin1a2lem12  9271  fin1a2lem13  9272  ttukeylem6  9374  fpwwe2lem12  9501  fpwwe2lem13  9502  fpwwe2  9503  winalim2  9556  wunex2  9598  tskord  9640  prlem934  9893  mulcmpblnr  9930  dedekind  10238  addid1  10254  cnegex  10255  negeu  10309  add20  10578  divdivdiv  10764  ltmul12a  10917  lemul12a  10919  lediv12a  10954  supaddc  11028  supmul1  11030  cru  11050  uzwo3  11821  xleadd1a  12121  xmullem  12132  xmulgt0  12151  xlemul1a  12156  ixxun  12229  ixxss12  12233  ioodisj  12340  fz0fzelfz0  12484  mulexpz  12940  leexp1a  12959  expmulnbnd  13036  hashf1  13279  fi1uzind  13317  brfi1indALT  13320  reuccats1  13526  abs3lem  14122  rexanre  14130  cau3lem  14138  limsupgre  14256  limsupbnd2  14258  o1lo1  14312  rlimclim1  14320  rlimclim  14321  rlimcn1  14363  rlimcn2  14365  o1of2  14387  o1rlimmul  14393  lo1add  14401  lo1mul  14402  isercolllem1  14439  climcau  14445  caucvgrlem  14447  caucvgb  14454  summolem2  14491  summo  14492  modfsummod  14570  o1fsum  14589  prodmolem2  14709  addmodlteqALT  15094  rpdvds  15421  isprm5  15466  isprm6  15473  pclem  15590  pcqmul  15605  pcexp  15611  pcneg  15625  pcprmpw2  15633  pcadd  15640  pcmpt  15643  4sqlem13  15708  vdwlem2  15733  vdwlem7  15738  vdwlem12  15743  ramval  15759  ramub2  15765  ramz2  15775  ramcl  15780  cshwshashlem2  15850  imasval  16218  imasdsval  16222  mreexexd  16355  mreexexdOLD  16356  acsfn  16367  issubc3  16556  idfucl  16588  funcres2c  16608  isnat  16654  fucpropd  16684  xpcval  16864  xpcco  16870  prfval  16886  evlf2  16905  evlfcl  16909  curf12  16914  curf1cl  16915  curf2  16916  curfcl  16919  curf2ndf  16934  hof2val  16943  hofcl  16946  hofpropd  16954  yonedalem4a  16962  yonedainv  16968  drsdirfi  16985  pospo  17020  poslubmo  17193  posglbmo  17194  isipodrs  17208  acsinfd  17227  gsumvalx  17317  gsumpropd2lem  17320  ismndd  17360  mndpropd  17363  mhmeql  17411  mrcmndind  17413  frmdup3lem  17450  mhmmnd  17584  issubg4  17660  ssnmz  17683  conjnmzb  17742  f1otrspeq  17913  psgneu  17972  pgpfi  18066  sylow2blem3  18083  slwhash  18085  fislw  18086  sylow3lem2  18089  lsmdisj2  18141  pj1eu  18155  efgredlem  18206  frgpuplem  18231  gexex  18302  frgpnabl  18324  dprdfadd  18465  dpjidcl  18503  pgpfac1lem3  18522  pgpfaclem3  18528  ablfac2  18534  ringpropd  18628  islmhm2  19086  lmhmpropd  19121  lbsextlem4  19209  assapropd  19375  psrval  19410  evlslem1  19563  prmirredlem  19889  psgndiflemA  19995  lsmcss  20084  uvcf1  20179  frlmsslsp  20183  frlmup1  20185  mamucl  20255  mamuass  20256  mamudi  20257  mamudir  20258  mamuvs1  20259  mamuvs2  20260  mamulid  20295  mamurid  20296  dmatsubcl  20352  dmatmulcl  20354  scmatscm  20367  marrepval  20416  marepveval  20422  mdetunilem7  20472  gsummatr01lem4  20512  cpmatmcllem  20571  mat2pmatf1  20582  mat2pmatlin  20588  decpmatmul  20625  pm2mpmhmlem2  20672  chpidmat  20700  pptbas  20860  toponmre  20945  restbas  21010  iscncl  21121  cnrest2  21138  cnpdis  21145  lmcnp  21156  dishaus  21234  cmpcovf  21242  tgcmp  21252  dfconn2  21270  clsconn  21281  2ndcctbss  21306  dis2ndc  21311  1stccnp  21313  islly2  21335  cldllycmp  21346  locfincmp  21377  comppfsc  21383  kgentopon  21389  txcls  21455  ptpjopn  21463  dfac14  21469  xkoccn  21470  txcnp  21471  txcmpb  21495  txlm  21499  xkopt  21506  xkoco1cn  21508  xkoco2cn  21509  qtopcn  21565  qtoprest  21568  regr1lem2  21591  xkocnv  21665  qtophmeo  21668  fmfnfmlem4  21808  hausflim  21832  hauspwpwf1  21838  fclscmp  21881  alexsublem  21895  alexsubALTlem2  21899  alexsubALTlem3  21900  ptcmplem3  21905  ptcmplem4  21906  ptcmplem5  21907  cnextfun  21915  tmdgsum2  21947  symgtgp  21952  tsmsval2  21980  tsmsgsum  21989  utoptop  22085  ismet2  22185  blin  22273  metss2lem  22363  methaus  22372  met1stc  22373  met2ndci  22374  prdsxmslem2  22381  metcnp3  22392  metcnpi3  22398  metustto  22405  metustfbas  22409  nlmvscn  22538  nrginvrcn  22543  xrsxmet  22659  reconnlem1  22676  reconn  22678  xrge0tsms  22684  xmetdcn2  22687  metdscn  22706  addcnlem  22714  fsumcn  22720  cnheiborlem  22800  cnheibor  22801  bndth  22804  lebnum  22810  nmoleub2lem2  22962  ipcn  23091  iscmet3  23137  caubl  23152  rrxdstprj1  23238  minveclem3b  23245  minveclem7  23252  pjthlem2  23255  pmltpc  23265  volfiniun  23361  ioombl1  23376  dyadss  23408  dyaddisjlem  23409  dyadmax  23412  dyadmbllem  23413  opnmbllem  23415  itg1addlem2  23509  itg10a  23522  mbfi1fseqlem6  23532  itg2seq  23554  itg2monolem1  23562  itg2gt0  23572  itgfsum  23638  limcfval  23681  ellimc2  23686  ellimc3  23688  limcres  23695  limciun  23703  dvres  23720  dveflem  23787  rolle  23798  dvlip2  23803  c1liplem1  23804  dvgt0lem1  23810  dvgt0  23812  dvlt0  23813  dvne0  23819  dvfsumrlimge0  23838  ftc1lem6  23849  itgsubst  23857  mdegmullem  23883  ply1domn  23928  ply1divex  23941  fta1g  23972  fta1b  23974  plyf  23999  dgrlem  24030  coeid  24039  plydivalg  24099  aannenlem1  24128  aalioulem3  24134  aalioulem6  24137  abelthlem8  24238  efif1olem4  24336  chordthm  24609  xrlimcnp  24740  jensen  24760  lgamcvglem  24811  lgamcvg2  24826  sqf11  24910  fsumvma2  24984  perfectlem2  25000  lgsdilem  25094  lgsquad2lem2  25155  lgsquad3  25157  2sqlem5  25192  2sqlem9  25197  2sqb  25202  rpvmasumlem  25221  dchrisum0flb  25244  dchrisum0  25254  pntpbnd  25322  pntibndlem3  25326  pntleml  25345  legov  25525  legtrid  25531  tglinethru  25576  tglnpt2  25581  tglineintmo  25582  mirreu3  25594  perpcom  25653  colperpexlem3  25669  mideu  25675  opphllem1  25684  hlpasch  25693  lnopp2hpgb  25700  trgcopy  25741  brcgr  25825  brbtwn2  25830  colinearalg  25835  axsegcon  25852  axeuclidlem  25887  axcontlem9  25897  ecgrtg  25908  elntg  25909  eengtrkg  25910  upgr1eopALT  26057  usgredg4  26154  subuhgr  26223  subumgr  26225  usgr2wspthon  26932  eupth2lems  27216  n4cyclfrgr  27271  vacn  27677  blocni  27788  ubthlem3  27856  minvecolem7  27867  chocunii  28288  pjhthmo  28289  pjhthlem2  28379  kbass5  29107  mdsymlem5  29394  foresf1o  29469  fcobij  29628  xrofsup  29661  archirngz  29871  archiabllem2a  29876  xrge0tsmsd  29913  isarchiofld  29945  smatrcl  29990  reff  30034  ordtconnlem1  30098  qqhval2  30154  volmeas  30422  fiunelcarsg  30506  ballotlemfc0  30682  ballotlemfcc  30683  signstfvneq0  30777  derangenlem  31279  erdsze2lem1  31311  pconnconn  31339  connpconn  31343  cvxsconn  31351  cvmliftmolem2  31390  cvmliftmo  31392  cvmlift2lem10  31420  cvmlift2lem12  31422  cvmlift3lem7  31433  mrsubff1  31537  msubff1  31579  frpomin  31863  poseq  31878  nolt02o  31970  noprefixmo  31973  nosupbnd2  31987  noetalem3  31990  noetalem5  31992  conway  32035  slerec  32048  ifscgr  32276  cgrxfr  32287  btwnconn1lem13  32331  btwnconn1lem14  32332  outsideofeq  32362  ellines  32384  finminlem  32437  fnejoin2  32489  unbdqndv2  32627  poimirlem13  33552  poimirlem14  33553  poimirlem32  33571  opnmbllem0  33575  mblfinlem3  33578  itg2addnclem  33591  itg2addnc  33594  ftc1cnnc  33614  upixp  33654  filbcmb  33665  sstotbnd2  33703  isbnd3  33713  prdsbnd2  33724  cntotbnd  33725  ismtyima  33732  bfp  33753  rrncmslem  33761  unichnidl  33960  lshpcmp  34593  islshpat  34622  lfl0f  34674  ishlat3N  34959  3dim1  35071  islvol5  35183  lvoli2  35185  lncvrelatN  35385  pclfinclN  35554  pexmidlem8N  35581  idltrn  35754  cdleme42keg  36091  cdleme42mgN  36093  cdlemf2  36167  cdlemg2cex  36196  trlcoat  36328  dihopelvalcpre  36854  dih1dimatlem  36935  dihjatcclem4  37027  lcfl7N  37107  lcfrlem9  37156  mapdh9a  37396  hdmapglem7  37538  nacsfix  37592  mzpsubst  37628  mzpcompact2lem  37631  eldioph2lem2  37641  eldioph2  37642  eldioph2b  37643  diophin  37653  diophun  37654  irrapxlem3  37705  irrapxlem5  37707  pell1234qrreccl  37735  pell1234qrmulcl  37736  pell14qrdich  37750  pell1qrge1  37751  pell1qrgaplem  37754  monotuz  37823  rpexpmord  37830  acongtr  37862  acongrep  37864  jm2.23  37880  jm2.26a  37884  jm2.26lem3  37885  jm2.26  37886  jm2.27  37892  wepwsolem  37929  fnwe2lem2  37938  kelac1  37950  kercvrlsm  37970  hbtlem5  38015  hbt  38017  mpaaeu  38037  rfovcnvf1od  38615  cncmpmax  39505  rfcnnnub  39509  disjxp1  39552  iccintsng  40067  fprodcn  40150  lptioo2  40181  lptioo1  40182  limclner  40201  stoweidlem31  40566  stoweidlem34  40569  stoweidlem35  40570  stoweidlem49  40584  stoweidlem59  40594  stoweidlem62  40597  fourierdlem60  40701  fourierdlem61  40702  fourierdlem87  40728  iundjiun  40995  ismeannd  41002  hoidmvle  41135  smfsuplem2  41339  reuccatpfxs1  41759  perfectALTVlem2  41956  mogoldbb  41998  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  mgmhmeql  42128  mndpsuppss  42477  scmsuppss  42478  lindslinindsimp2lem5  42576  elfzolborelfzop1  42634  elbigolo1  42676
  Copyright terms: Public domain W3C validator