MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anbi12d Unicode version

Theorem anbi12d 691
Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bi12d.1  |-  ( ph  ->  ( ps  <->  ch )
)
bi12d.2  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
anbi12d  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  ta ) ) )

Proof of Theorem anbi12d
StepHypRef Expression
1 bi12d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21anbi1d 685 . 2  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
3 bi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43anbi2d 684 . 2  |-  ( ph  ->  ( ( ch  /\  th )  <->  ( ch  /\  ta ) ) )
52, 4bitrd 244 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  pm4.38  842  3anbi123d  1252  cadbi123d  1373  drsb1  1975  mopick  2218  clelab  2416  cbvreu  2775  cbvrexdva2  2782  cbvrab  2799  gencbvex  2843  rspce  2892  eqvincf  2909  ceqsrexv  2914  elrabf  2935  rexab2  2945  reu2  2966  reu6  2967  rmo4  2971  reu8  2974  reuind  2981  sbcan  3046  sbcang  3047  sbcabel  3081  rmob  3092  cbvreucsf  3158  cbvrabcsf  3159  difjust  3167  injust  3171  eldif  3175  psseq1  3276  psseq2  3277  ssconb  3322  elin  3371  pssdifcom1  3552  pssdifcom2  3553  2ralunsn  3832  elunii  3848  csbunig  3851  eluniab  3855  disjprg  4035  disjxun  4037  cbvopab  4103  cbvopab1  4105  cbvopab2  4106  cbvopab1s  4107  cbvopab2v  4109  cbvmpt  4126  trel  4136  nalset  4167  elssabg  4182  intabs  4188  nnullss  4251  exss  4252  oteqex  4275  opelopab2a  4296  dfid3  4326  poeq1  4333  pocl  4337  soeq1  4349  fri  4371  weeq1  4397  weeq2  4398  ordeq  4415  zfun  4529  snnex  4540  reusv3  4558  onminex  4614  dflim3  4654  csbxpg  4732  vtoclr  4749  opeliunxp  4756  poinxp  4769  wesn  4777  opbrop  4783  opeliunxp2  4840  relop  4850  elrnmpt1  4944  elsnres  5007  dfres2  5018  asymref2  5076  elxp4  5176  elxp5  5177  funopg  5302  fununi  5332  funcnvuni  5333  fneq1  5349  2elresin  5371  feq1  5391  f1eq1  5448  foeq1  5463  f1oeq1  5479  f1oeq2  5480  f1oeq3  5481  ffoss  5521  brprcneu  5534  fv3  5557  tz6.12f  5562  ssimaex  5600  dffv2  5608  fvopab3g  5614  fvopab3ig  5615  fvopab6  5637  fmptco  5707  opabex3  5785  elunirnALT  5795  f1imaeq  5805  f1imapss  5806  foeqcnvco  5820  fliftfun  5827  fliftval  5831  isoeq1  5832  isoeq4  5835  isomin  5850  isoini  5851  isofrlem  5853  isopolem  5858  isowe  5862  f1oiso2  5865  f1oweALT  5867  cbvoprab1  5934  cbvoprab2  5935  cbvoprab12  5936  cbvmpt2x  5940  ov  5983  ovig  5985  ovg  6002  caoftrn  6128  unielxp  6174  dfoprab4  6193  dfoprab4f  6194  exopxfr2  6200  fmpt2x  6206  frxp  6241  xporderlem  6242  poxp  6243  fnwelem  6246  fnse  6248  dftpos4  6269  tpostpos  6270  cbvriota  6331  riotasv2d  6365  smoiso  6395  tfrlem1  6407  tfrlem3  6409  tfrlem3a  6410  tfrlem5  6412  tfrlem12  6421  omeu  6599  oeoa  6611  oeoe  6613  oeeui  6616  nnacan  6642  nnmcan  6648  ertr  6691  brecop  6767  eroveu  6769  erov  6771  ecopovtrn  6777  th3qlem1  6780  th3qlem2  6781  th3q  6783  elpm2r  6804  mapsncnv  6830  elixp2  6836  ixpeq1  6843  elixpsn  6871  ixpsnf1o  6872  mapsnen  6954  map1  6955  xpsnen  6962  endisj  6965  pw2f1olem  6982  sbthlem2  6988  sbth  6997  disjenex  7035  domssex2  7037  domssex  7038  xpf1o  7039  mapunen  7046  php2  7062  nnsdomo  7071  isinf  7092  ac6sfi  7117  unfilem1  7137  fiint  7149  dffi2  7192  dffi3  7200  marypha1lem  7202  supeq1  7214  supmo  7219  eqsup  7223  supmaxlem  7231  supisolem  7237  supisoex  7238  oieq1  7243  oieq2  7244  oieu  7270  hartogslem1  7273  wemaplem1  7277  wemaplem2  7278  wemapso2lem  7281  wdom2d  7310  inf0  7338  axinf2  7357  dfom3  7364  cantnfle  7388  cantnfrescl  7394  oemapval  7401  cantnflem1  7407  cantnf  7411  wemapwe  7416  tz9.1c  7428  tctr  7441  tcmin  7442  tc2  7443  rankr1c  7509  rankonidlem  7516  tcrank  7570  karden  7581  cardprclem  7628  carden2  7636  cardsdom2  7637  infxpen  7658  infxpenc2lem1  7662  fseqenlem1  7667  fseqdom  7669  ac5num  7679  acneq  7686  acni2  7689  aleph11  7727  aceq1  7760  aceq0  7761  aceq2  7762  aceq3lem  7763  dfac3  7764  dfac4  7765  dfac5lem1  7766  dfac5lem2  7767  dfac5lem3  7768  dfac5lem4  7769  dfac5  7771  dfac2a  7772  dfac2  7773  dfac9  7778  dfacacn  7783  kmlem1  7792  kmlem2  7793  kmlem4  7795  kmlem14  7805  infpss  7859  ackbij2  7885  cflem  7888  cfval  7889  cflecard  7895  cfeq0  7898  cfsuc  7899  cfflb  7901  cfslb  7908  cfsmolem  7912  cfcoflem  7914  coftr  7915  sornom  7919  fin2i  7937  isfin4  7939  fin4i  7940  isfin2-2  7961  enfin2i  7963  fin23lem32  7986  fin23lem34  7988  fin23lem35  7989  fin23lem41  7994  isf32lem9  8003  fin1a2lem6  8047  axcc2lem  8078  axcc3  8080  axcc4dom  8083  domtriomlem  8084  dominf  8087  axdc2lem  8090  axdc2  8091  axdc3lem2  8093  axdc3lem4  8095  zfac  8102  ac7g  8117  ac5  8120  ac6num  8122  ac6sg  8131  zorn2lem7  8145  ttukeylem7  8158  brdom3  8169  brdom7disj  8172  brdom6disj  8173  dominfac  8211  axrepndlem2  8231  axunnd  8234  axregndlem2  8241  axinfndlem1  8243  axinfnd  8244  axacndlem5  8249  axacnd  8250  zfcndun  8253  zfcndac  8257  elgch  8260  gchi  8262  engch  8266  fpwwe2cbv  8268  fpwwe2lem2  8270  fpwwe2lem8  8275  fpwwe2lem12  8279  fpwwe2  8281  fpwwecbv  8282  fpwwelem  8283  pwfseqlem1  8296  pwfseqlem4a  8299  pwfseqlem4  8300  wunex2  8376  eltskg  8388  inar1  8413  tskuni  8421  elgrug  8430  grothac  8468  indpi  8547  nqereu  8569  enqeq  8574  ltsonq  8609  ltbtwnnq  8618  elnp  8627  elnpi  8628  prcdnq  8633  ltprord  8670  ltsopr  8672  ltexprlem4  8679  ltexprlem7  8682  reclem2pr  8688  reclem3pr  8689  supexpr  8694  ltsosr  8732  supsrlem  8749  ltresr  8778  axcnre  8802  axpre-lttrn  8804  axpre-sup  8807  axlttrn  8911  axsup  8914  letri3  8923  readdcan  9002  le2add  9272  ltleadd  9273  lt2sub  9288  le2sub  9289  mulge0  9307  eqord1  9317  wloglei  9321  msq11  9673  lbinfm  9723  sup2  9726  infm3  9729  dfinfmr  9747  cju  9758  dfnn2  9775  dfnn3  9776  nn2ge  9787  nominpos  9964  nnunb  9977  elz2  10056  dfuzi  10118  uzind  10119  uzindOLD  10122  zsupss  10323  uzsupss  10326  zmax  10329  rebtwnz  10331  xrltlen  10496  xrletri3  10502  z2ge  10541  qbtwnre  10542  qbtwnxr  10543  xmulval  10568  xrsupsslem  10641  xrinfmsslem  10642  xrsupss  10643  xrinfmss  10644  elixx1  10681  ixxin  10689  elioo2  10713  icc0  10720  iooshf  10744  iooneg  10772  iccneg  10773  icoshft  10774  elfz1  10803  fzrev  10862  flval  10942  fllelt  10945  flval2  10960  flbi  10962  flbi2  10963  modid2  11010  axdc4uz  11061  seqf1o  11103  nnesq  11241  hashsdom  11379  hashbclem  11406  hashf1lem1  11409  seqcoll  11417  shftlem  11579  shftfib  11583  shftfn  11584  2shfti  11591  cjval  11603  cjth  11604  remim  11618  cnpart  11741  01sqrex  11751  resqrex  11752  sqrmo  11753  absdiflt  11817  absdifle  11818  abs1m  11835  rexanuz2  11849  cau3lem  11854  sqreu  11860  clim  11984  rlim  11985  clim2  11994  o1lo1  12027  climshftlem  12064  addcn2  12083  lo1add  12116  lo1mul  12117  isercoll  12157  climcau  12160  caurcvg2  12166  sumeq1f  12177  cbvsum  12184  summolem2  12205  summo  12206  zsum  12207  fsum  12209  fsum2dlem  12249  fsumcom2  12253  fsum00  12272  reef11  12415  sin01bnd  12481  cos01bnd  12482  cpnnen  12523  ruclem9  12532  divalgmod  12621  ndvdssub  12622  smufval  12684  smupp1  12687  gcdcllem2  12707  gcdcllem3  12708  gcddvds  12710  gcddiv  12744  isprm3  12783  qredeu  12802  isprm5  12807  qnumdencl  12826  qnumdenbi  12831  crt  12862  eulerthlem2  12866  pythagtriplem19  12902  pceu  12915  pczpre  12916  pcdiv  12921  pc11  12948  prmpwdvds  12967  pockthi  12970  infpnlem2  12974  infpn2  12976  prmreclem2  12980  prmreclem4  12982  prmreclem5  12983  elgz  12994  vdwapun  13037  vdwpc  13043  vdwlem2  13045  vdwlem6  13049  vdwlem8  13051  ramval  13071  0ram  13083  ramz2  13087  ramub1lem1  13089  ramcl  13092  prdsval  13371  f1ocpbllem  13442  ercpbl  13467  erlecpbl  13468  xpsle  13499  ismre  13508  mreexexlemd  13562  mreexexlem3d  13564  mreexexlem4d  13565  isacs  13569  isacs2  13571  isacs1i  13575  mreacs  13576  iscat  13590  iscatd  13591  catidex  13592  catideu  13593  cidfval  13594  cidval  13595  catidd  13598  iscatd2  13599  catpropd  13628  cidpropd  13629  isepi  13659  sectffval  13669  sectfval  13670  brssc  13707  isssc  13713  issubc  13728  isfunc  13754  funcres2b  13787  funcpropd  13790  isfull  13800  isfth  13804  fthpropd  13811  fthinv  13816  fullres2c  13829  ffthres2c  13830  fucinv  13863  setcsect  13937  setcinv  13938  isprs  14080  prslem  14081  isdrs  14084  ispos  14097  posi  14100  isposd  14105  lubfval  14128  lubval  14129  lubprop  14130  glbfval  14133  glbval  14134  glbprop  14135  joinval2  14139  joinlem  14140  joinle  14143  meetval2  14146  meetlem  14147  meetle  14150  islat  14169  latlem  14170  isclat  14231  clatlem  14232  clatl  14236  isglbd  14237  lubun  14243  pospropd  14254  odulatb  14263  oduclatb  14264  poslubmo  14266  poslubd  14267  ipole  14277  ipopos  14279  isipodrs  14280  ipodrsima  14284  mreclat  14306  pslem  14331  spwval2  14349  spwmo  14351  spwpr2  14353  spwpr4  14356  isla  14358  letsr  14365  isdir  14370  dirtr  14374  dirge  14375  ismnd  14385  mgmidmo  14386  mndlem1  14387  grpidval  14400  ismgmid  14403  mgmlrid  14405  ismgmid2  14406  ismndd  14412  mndpropd  14414  grpidpropd  14415  ismhm  14433  mhmpropd  14437  issubm  14441  gsumvallem1  14464  gsumvallem2  14465  gsumvalx  14467  gsumpropd  14469  gsumress  14470  gsumval2a  14475  grppropd  14516  isgrpid2  14534  isgrpinv  14548  grplactcnv  14580  0subg  14658  cycsubgcl  14659  eqgfval  14681  eqgval  14682  isghm  14699  ghmrn  14712  resghm  14715  ghmpropd  14736  gicsubgen  14758  isga  14761  resscntz  14823  oppgsubg  14852  sylow1  14930  slwispgp  14938  pgpssslw  14941  sylow2blem2  14948  lsmsubm  14980  lsmcntzr  15005  lsmdisj3a  15014  lsmdisj3b  15015  pj1ghm  15028  efglem  15041  efgval  15042  efgsdm  15055  efgrelexlemb  15075  efgcpbllemb  15080  frgpmhm  15090  frgpuplem  15097  cmnpropd  15114  ablpropd  15115  divsabl  15173  frgpnabllem1  15177  gsumval3eu  15206  gsumval3  15207  dmdprd  15252  dprdsubg  15275  subgdmdprd  15285  dmdprdpr  15300  pgpfac1lem1  15325  pgpfac1lem3  15328  pgpfac1lem5  15330  pgpfac1  15331  pgpfaclem1  15332  pgpfaclem2  15333  pgpfaclem3  15334  ablfaclem2  15337  ablfaclem3  15338  isrng  15361  rngpropd  15388  crngpropd  15389  dvdsrval  15443  dvdsr  15444  unitgrp  15465  dvdsrpropd  15494  unitpropd  15495  isnirred  15498  isdrngd  15553  isdrngrd  15554  fldpropd  15556  issubrg  15561  subrg1  15571  subrgpropd  15595  rhmpropd  15596  abvfval  15599  isabv  15600  abvpropd  15623  issrng  15631  issrngd  15642  islmod  15647  lmodlema  15648  islmodd  15649  lmodprop2d  15703  islmhm  15800  lmhmpropd  15842  islbs  15845  lsmspsn  15853  lbspropd  15868  lvecindp2  15908  lbsextlem1  15927  lbsextlem3  15929  lbsextlem4  15930  lvecprop2d  15935  lvecpropd  15936  divscrng  16008  lidldvgen  16023  isassa  16072  assalem  16073  isassad  16079  assapropd  16083  ltbval  16229  opsrval  16232  zntoslem  16526  isphl  16548  isphld  16574  isobs  16636  istopg  16657  eltopspOLD  16672  istpsOLD  16674  fiinbas  16706  eltg2  16712  topbas  16726  pptbas  16761  clsval2  16803  elcls  16826  isclo  16840  neiint  16857  neips  16866  opnneissb  16867  opnssneib  16868  innei  16878  restbas  16905  restcld  16919  ordtbas2  16937  leordtval  16959  cnpnei  17009  cnconst2  17027  cnpresti  17032  cnprest  17033  cnpdis  17037  lmss  17042  lmres  17044  ordtt1  17123  cmpcovf  17134  cmpsublem  17142  cmpsub  17143  hauscmplem  17149  concompid  17173  concompcon  17174  concompss  17175  1stcfb  17187  2ndci  17190  2ndcsb  17191  2ndc1stc  17193  1stcrest  17195  2ndcctbss  17197  2ndcomap  17200  2ndcsep  17201  dis2ndc  17202  nllyi  17217  restlly  17225  islly2  17226  lly1stc  17238  dislly  17239  llycmpkgen2  17261  txbas  17278  eltx  17279  ptval  17281  elpt  17283  ptpjopn  17322  txcnp  17330  ptcnplem  17331  txcnmpt  17334  uptx  17335  txdis  17342  txdis1cn  17345  txlly  17346  txtube  17350  txhaus  17357  txlm  17358  tx1stc  17360  txkgen  17362  xkohaus  17363  xkococnlem  17369  basqtop  17418  qtopcld  17420  kqreglem1  17448  kqreglem2  17449  kqnrmlem1  17450  kqnrmlem2  17451  reghmph  17500  nrmhmph  17501  txhmeo  17510  pt1hmeo  17513  ptuncnv  17514  fbssfi  17548  isfildlem  17568  isfild  17569  elfg  17582  filuni  17596  uffix  17632  fmfnfm  17669  flimval  17674  flimcls  17696  hauspwpwf1  17698  txflf  17717  fclscf  17736  fclsfnflim  17738  alexsublem  17754  alexsubALTlem1  17757  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  ptcmplem3  17764  tmdgsum2  17795  symgtgp  17800  subgntr  17805  opnsubg  17806  tgpconcompeqg  17810  ghmcnp  17813  divstgpopn  17818  divstgplem  17819  tsmsgsum  17837  tsmsxplem1  17851  istlm  17883  ismet  17904  isxmet  17905  imasdsf1olem  17953  imasf1oxmet  17955  bldisj  17971  blin  17986  blssex  17989  ssblex  17990  xmspropd  18035  mspropd  18036  setsms  18042  neibl  18063  blcld  18067  metequiv  18071  stdbdmopn  18080  met1stc  18083  met2ndci  18084  metrest  18086  prdsxmslem2  18091  metcnp3  18102  dscopn  18112  ngptgp  18168  ngppropd  18169  isnlm  18202  nlmvscnlem1  18213  nlmvscn  18214  tgioo  18318  tgqioo  18322  zdis  18338  xrge0tsms  18355  xmetdcn2  18358  addcnlem  18384  icoopnst  18453  iocopnst  18454  xrhmeo  18460  cnheibor  18469  ishtpy  18486  htpyi  18488  isphtpy  18495  phtpyi  18498  isphtpc  18508  om1val  18544  om1elbas  18546  elpi1i  18560  isclm  18578  ipcnlem1  18688  ipcn  18689  lmmcvg  18703  iscau2  18719  equivcmet  18757  bcthlem1  18762  bcth  18767  cmspropd  18787  srabn  18793  minveclem3b  18808  minveclem7  18815  pmltpclem1  18824  ivthlem2  18828  ovolctb  18865  ovolunlem1  18872  ovolfiniun  18876  ovoliunlem2  18878  ovoliunlem3  18879  ovoliunnul  18882  ovolshftlem1  18884  ovolscalem1  18888  ovolicc1  18891  volfiniun  18920  voliunlem1  18923  ioorcl  18948  dyaddisj  18967  volivth  18978  vitalilem3  18981  vitali  18984  ismbf1  18997  ismbfcn  19002  ismbfcn2  19010  mbfeqa  19014  mbfmax  19020  mbfimaopnlem  19026  mbfaddlem  19031  i1faddlem  19064  i1fmullem  19065  mbfi1fseqlem4  19089  mbfi1fseqlem6  19091  mbfi1flimlem  19093  itg2lr  19101  itg2seq  19113  itg2i1fseq  19126  itg2addlem  19129  isibl  19136  isibl2  19137  cbvitg  19146  iblcnlem1  19158  iblcnlem  19159  iblrelem  19161  iblre  19164  iblcn  19169  itgeqa  19184  itgfsum  19197  ellimc2  19243  limcnlp  19244  ellimc3  19245  limcflf  19247  limciun  19260  dvbsss  19268  dvferm1lem  19347  dvferm2lem  19349  dvlip2  19358  dvcvx  19383  ftc1a  19400  evlseu  19416  mpfrcl  19418  evlsval  19419  evlsval2  19420  evl1vsd  19436  mpfind  19444  mdegmullem  19480  deg1ldg  19494  uc1pval  19541  isuc1p  19542  mon1pval  19543  ismon1p  19544  q1peqb  19556  elply2  19594  coeeu  19623  coelem  19624  coeeq  19625  plydivlem4  19692  fta1lem  19703  fta1  19704  vieta1lem2  19707  vieta1  19708  plyexmo  19709  aannenlem2  19725  aaliou3lem7  19745  aaliou3lem9  19746  sincosq1sgn  19882  sincosq2sgn  19883  sincosq3sgn  19884  sincosq4sgn  19885  cos11  19911  efopn  20021  cxpcn3lem  20103  cxpcn3  20104  logreclem  20132  dcubic2  20156  dcubic  20158  quart  20173  atandm2  20189  atans2  20243  dmarea  20268  xrlimcnp  20279  jensen  20299  wilthlem2  20323  wilthlem3  20324  wilth  20325  vmappw  20370  mumullem2  20434  sqff1o  20436  musum  20447  chpchtsum  20474  perfect  20486  dchrptlem1  20519  bpos1lem  20537  bposlem9  20547  lgsval  20555  lgsqrlem1  20596  lgsquadlem1  20609  lgsquadlem2  20610  lgsquadlem3  20611  lgsquad  20612  2sqlem8a  20626  2sqlem8  20627  2sqlem9  20628  2sqlem11  20630  2sq  20631  dchrisumlema  20653  dchrisumlem2  20655  dchrmusumlema  20658  dchrisum0lema  20679  dchrisum0lem1  20681  pntpbnd1  20751  pntpbnd2  20752  pntibndlem2  20756  pntibndlem3  20757  pntibnd  20758  pntlemi  20769  pntlemp  20775  pnt3  20777  isgrpo  20879  isgrpo2  20880  isgrpoi  20881  grpoideu  20892  gidval  20896  grpoidinv2  20901  grpoinv  20910  isgrpda  20980  isabloda  20982  isexid  21000  exidu1  21009  cmpidelt  21012  issmgrp  21017  elghomlem1  21044  elghomlem2  21045  ghgrp  21051  ghablo  21052  isrngo  21061  isrngod  21062  rngoid  21066  rngoideu  21067  cnrngo  21086  drngoi  21090  isdivrngo  21114  vci  21120  isvclem  21149  vacn  21283  smcnlem  21286  nmosetn0  21359  nmoolb  21365  nmounbseqi  21371  nmounbseqiOLD  21372  nmlno0lem  21387  ajmoi  21453  minvecolem7  21478  htth  21514  normlem7tALT  21714  norm3lemt  21747  hlimi  21783  issh2  21804  chlimi  21830  hhsssh  21862  ocsh  21878  ocin  21891  pjhthmo  21897  shintcl  21925  chintcl  21927  omlsi  21999  pjoml  22031  chpsscon3  22098  cmbr  22179  pjoml6i  22184  cm2j  22215  spansncv  22248  adjmo  22428  eigre  22431  eigorth  22434  nmopsetn0  22461  elunop  22468  nmfnsetn0  22474  nmoplb  22503  nmfnlb  22520  nmlnop0iALT  22591  lnophm  22615  nmcexi  22622  nmbdfnlb  22646  branmfn  22701  rnbra  22703  leopg  22718  leoptri  22732  leoptr  22733  opsqrlem1  22736  hmopidmch  22749  hmopidmpj  22750  dfpjop  22778  isst  22809  ishst  22810  hstel2  22815  jpi  22866  cvbr  22878  cvcon3  22880  cvnbtwn  22882  mdbr  22890  dmdbr  22895  mdsl1i  22917  mdslmd1lem3  22923  mdslmd1lem4  22924  csmdsymi  22930  elat2  22936  chrelati  22960  chrelat2i  22961  cvexchlem  22964  chirred  22991  atcvat4i  22993  mdsymlem2  23000  mdsymlem8  23006  mddmdin0i  23027  cdj1i  23029  cdj3i  23037  rmo4fOLD  23195  xppreima  23226  rabfmpunirn  23232  cbvmptf  23235  fmptcof2  23244  iocinioc2  23287  tpr2rico  23311  cnvordtrestixx  23312  cbvdisjf  23365  gsumpropd2lem  23394  xrge0tsmsd  23397  esumcvg  23469  sigaval  23486  issiga  23487  isrnsigaOLD  23488  isrnsiga  23489  issgon  23499  measvun  23552  isanmbfm  23576  dya2iocseg  23594  isibfm  23608  derangval  23713  derangenlem  23717  subfacp1lem3  23728  subfacp1lem5  23730  subfacp1lem6  23731  subfacp1  23732  subfacval2  23733  erdszelem1  23737  erdsze  23748  erdsze2lem2  23750  kur14lem9  23760  kur14  23762  cnpcon  23776  txpcon  23778  ptpcon  23779  indispcon  23780  conpcon  23781  cvxpcon  23788  cnllyscon  23791  cvmscbv  23804  iscvm  23805  cvmcov  23809  cvmsi  23811  cvmsval  23812  cvmsss2  23820  cvmcov2  23821  cvmopnlem  23824  cvmliftmo  23830  cvmliftlem10  23840  cvmliftlem14  23843  cvmliftlem15  23844  cvmliftiota  23847  cvmlift2lem4  23852  cvmlift2lem13  23861  cvmlift2  23862  cvmliftphtlem  23863  cvmlift3lem2  23866  cvmlift3lem6  23870  cvmlift3lem7  23871  cvmlift3lem9  23873  cvmlift3  23874  iseupa  23896  relexpindlem  24051  rtrclreclem.trans  24058  dedekind  24097  dedekindle  24098  mulsuble0b  24103  prodmolem2  24158  prodmo  24159  zprodn0  24162  fprod  24164  dfpo2  24183  fununiq  24197  mpteq12d  24199  dfdm5  24203  dfrn5  24204  dfon2lem3  24212  dfon2lem4  24213  dfon2lem5  24214  dfon2lem6  24215  dfon2lem7  24216  dfon2lem8  24217  dfon2  24219  frmin  24313  poseq  24324  soseq  24325  wfr3g  24326  wfrlem1  24327  wfrlem4  24330  wfrlem12  24338  wfrlem15  24341  frr3g  24351  frrlem1  24352  frrlem4  24355  frrlem11  24364  sltval  24372  sltval2  24381  sltres  24389  nodense  24414  nocvxminlem  24415  nobndup  24425  nobnddown  24426  nofulllem1  24427  nofulllem2  24428  nofulllem5  24431  dfbigcup2  24510  elfix  24514  dffix2  24516  elfuns  24525  dfiota3  24533  brimg  24547  funpartfun  24553  dfrdg4  24560  tfrqfree  24561  brbtwn  24599  brcgr  24600  brbtwn2  24605  axcgrtr  24615  axsegconlem1  24617  axsegcon  24627  ax5seg  24638  axpasch  24641  axcontlem1  24664  axcontlem4  24667  axcontlem5  24668  axcontlem10  24673  brofs  24700  ofscom  24702  segconeu  24706  btwnswapid2  24713  btwnexch3  24715  btwnexch  24720  funtransport  24726  fvtransport  24727  transportprops  24729  brifs  24738  ifscgr  24739  cgr3tr4  24747  cgrxfr  24750  brcolinear2  24753  colineardim1  24756  brfs  24774  fscgr  24775  btwnconn1lem11  24792  btwnconn1lem13  24794  btwnconn1lem14  24795  brsegle  24803  seglecgr12  24806  seglerflx  24807  seglemin  24808  segletr  24809  segleantisym  24810  btwnsegle  24812  outsideoftr  24824  outsideofeq  24825  outsideofeu  24826  funray  24835  fvray  24836  linedegen  24838  fvline  24839  linethru  24848  hilbert1.1  24849  hilbert1.2  24850  lineintmo  24852  bpolyval  24856  limsucncmpi  24956  ltflcei  24998  lxflflp1  25000  ovoliunnfl  25001  ex-ovoliunnfl  25002  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  itg2gt0cn  25006  areacirclem6  25033  dfoprab4pop  25140  splint  25151  vxveqv  25157  ac5g  25178  injrec2  25222  repcpwti  25264  cbicp  25269  prjmapcp2  25273  islatalg  25286  cur1val  25301  isoriso  25315  isoriso2  25316  preotr2  25338  supdef  25365  inposet  25381  dffprod  25422  ridlideq  25438  rzrlzreq  25439  idlvalNEW  25548  isidlNEW  25549  vecval1b  25554  vecval3b  25555  svs2  25590  vri  25595  basexre  25625  osneisi  25634  intopcoaconb  25643  qusp  25645  intcont  25646  usptoplem  25649  istopx  25650  istopxc  25651  usptop  25653  prcnt  25654  iscnp4  25666  prdnei  25676  limptlimpr2lem1  25677  limptlimpr2lem2  25678  bwt2  25695  altretop  25703  trnij  25718  supnuf  25732  supexr  25734  distmlva  25791  tcnvec  25793  ismgra  25813  isalg  25824  algi  25830  isded  25839  dedi  25840  idosd  25847  iscatOLD  25857  cati  25858  cmpasso  25876  dualded  25886  ishoma  25890  ishomc  25892  ishomd  25893  imonclem  25916  iepiclem  25926  isiso  25928  cinvlem1  25931  cinvlem2  25932  cinvlem3  25933  isfuna  25937  isfunb  25938  issubcata  25949  infemb  25962  isinob  25965  issrc  25970  rocatval2  26063  setiscat  26082  indcls2  26099  pfsubkl  26150  bisig0  26165  lineval222  26182  lineval42  26183  lineval22  26185  lineval3a  26186  isconcl5ab  26205  isibg2  26213  isibg2aa  26215  isibg2aalem1  26216  isibg2aalem2  26217  isibg2aalem3  26218  sgplpte21b  26237  bosser  26270  isibcg  26294  trer  26330  finminlem  26334  isfne  26371  isref  26382  fness  26385  fneref  26387  fnessref  26396  refssfne  26397  islocfin  26399  finlocfin  26402  locfindis  26408  neibastop2lem  26412  neibastop3  26414  neifg  26423  tailfb  26429  filnetlem3  26432  filnetlem4  26433  unirep  26452  upixp  26506  indexdom  26516  sdclem2  26555  sdclem1  26556  sdc  26557  fdc  26558  fdc1  26559  istotbnd  26596  istotbnd3  26598  sstotbnd  26602  prdstotbnd  26621  cntotbnd  26623  ismtyval  26627  isismty  26628  heiborlem3  26640  heiborlem4  26641  heiborlem6  26643  heiborlem10  26647  rrnheibor  26664  reheibor  26666  exidcl  26669  exidreslem  26670  exidres  26671  exidresid  26672  ghomco  26676  divrngcl  26691  rngohomval  26698  isrngohom  26699  isriscg  26718  iscringd  26727  idlval  26741  isidl  26742  0idl  26753  keridl  26760  pridlval  26761  ispridl  26762  maxidlval  26767  ismaxidl  26768  smprngopr  26780  prnc  26795  ispridlc  26798  isdmn3  26802  prtlem10  26836  prtlem13  26839  prtlem15  26846  ismrcd2  26877  ismrc  26879  mzpclval  26906  elmzpcl  26907  mzpcl34  26912  mzpcompact2lem  26932  mzpcompact2  26933  diophrw  26941  eldioph2lem1  26942  eldioph2lem2  26943  eldioph3  26948  fz1eqin  26951  lzenom  26952  diophin  26955  diophun  26956  rexrabdioph  26978  eldioph4b  26997  fphpdo  27003  icodiamlt  27008  irrapxlem6  27015  pellexlem3  27019  pellex  27023  pell1qrval  27034  pell14qrval  27036  pell1234qrval  27038  pell1234qrreccl  27042  pell1234qrmulcl  27043  pell1234qrdich  27049  pell14qrmulcl  27051  pell14qrdich  27057  pell1qr1  27059  pellqrexplicit  27065  rmxycomplete  27105  rmxynorm  27106  2nn0ind  27133  rmxypos  27137  fzneg  27172  divalgmodcl  27183  jm2.23  27192  jm2.27  27204  rmydioph  27210  rmxdioph  27212  expdiophlem1  27217  expdiophlem2  27218  dford3lem2  27223  wepwsolem  27241  fnwe2val  27249  fnwe2lem2  27251  supeq123d  27261  aomclem8  27262  dsmmelbas  27308  enfixsn  27360  gicabl  27366  imasgim  27367  islindf  27385  lsslindf  27403  lsslinds  27404  hbtlem1  27430  hbtlem2  27431  hbtlem4  27433  hbtlem5  27435  dgraalem  27453  dgraaub  27456  aaitgo  27470  pmtrfrn  27503  psgnunilem2  27521  psgnunilem3  27522  psgnunilem4  27523  psgneu  27532  psgnvalii  27535  isdomn3  27626  sbiota1  27737  elunif  27790  rspcegf  27797  fnchoice  27803  fmul01  27813  climsuse  27837  stoweidlem7  27859  stoweidlem15  27867  stoweidlem16  27868  stoweidlem18  27870  stoweidlem27  27879  stoweidlem28  27880  stoweidlem31  27883  stoweidlem34  27886  stoweidlem36  27888  stoweidlem37  27889  stoweidlem41  27893  stoweidlem44  27896  stoweidlem45  27897  stoweidlem46  27898  stoweidlem48  27900  stoweidlem51  27903  stoweidlem52  27904  stoweidlem55  27907  stoweidlem57  27909  stoweidlem59  27911  stoweidlem60  27912  2reu4a  28070  sbcfun  28090  dfateq12d  28097  opabex3d  28190  sprmpt2  28207  isprmpt2  28208  usgraedgprv  28256  nb3gra2nb  28291  iscusgra  28292  cusgra2v  28297  istrl  28336  trlon  28339  istrlon  28340  trlonprop  28341  isspth  28355  pthon  28361  ispthon  28362  fargshiftf  28381  fargshiftf1  28382  eupatrl  28385  usgrcyclnl2  28387  constr3lem6  28395  3v3e3cycl2  28410  4cycl4v4e  28412  4cycl4dv  28413  4cycl4dv4e  28414  isfrgra  28417  frgra3vlem2  28425  frgra3v  28426  1vwmgra  28427  3vfriswmgralem  28428  3vfriswmgra  28429  3cyclfrgrarn1  28435  4cycl2vnunb  28439  bnj919  29113  bnj1185  29142  bnj66  29208  bnj1014  29308  bnj1015  29309  bnj1112  29329  bnj1228  29357  bnj1234  29359  bnj1321  29373  bnj1452  29398  bnj1463  29401  bnj1491  29403  drsb1NEW7  29483  lubunNEW  29785  lshpset  29790  islshp  29791  lsmsat  29820  lrelat  29826  lcvfbr  29832  lcvbr  29833  lcvnbtwn  29837  lsat0cv  29845  lcvexchlem1  29846  lcvexchlem4  29849  lcvexchlem5  29850  lkrpssN  29975  isopos  29992  opltcon3b  30016  omlfh3N  30071  cvrfval  30080  cvrval  30081  cvrnbtwn  30083  cvrcon3b  30089  cvrnbtwn4  30091  cvrcmp2  30096  isatl  30111  isat3  30119  iscvlat  30135  cvlexch1  30140  ishlat1  30164  glbconN  30188  hlsuprexch  30192  hlateq  30210  hlrelat  30213  hlrelat2  30214  cvrexchlem  30230  cvrat4  30254  3dim0  30268  3dim2  30279  2dim  30281  ps-2  30289  islln3  30321  llni2  30323  islpln5  30346  lplnexllnN  30375  lvoli3  30388  islvol5  30390  lvoli2  30392  4atlem3  30407  4atlem12  30423  islinei  30551  psubspset  30555  ispsubsp  30556  pmap11  30573  isline4N  30588  lnatexN  30590  pmapjoin  30663  pmapjat1  30664  psubclsetN  30747  ispsubclN  30748  ispsubcl2N  30758  lhprelat3N  30851  4atexlemex2  30882  4atex  30887  4atex2-0aOLDN  30889  4atex2-0cOLDN  30891  lautset  30893  islaut  30894  lautlt  30902  lautcvr  30903  pautsetN  30909  ispautN  30910  ltrnfset  30928  ltrnset  30929  ltrnatb  30948  cdleme0ex1N  31034  cdleme0nex  31101  cdleme18d  31106  cdleme25b  31165  cdleme25cv  31169  cdleme29b  31186  cdlemefrs29bpre0  31207  cdlemefr32sn2aw  31215  cdlemefs32sn1aw  31225  cdleme32fvaw  31250  cdleme40v  31280  cdleme42b  31289  cdleme46f2g1  31305  cdleme48gfv  31348  cdleme50eq  31352  cdlemg1fvawlemN  31384  cdlemk35s  31748  cdlemk39s  31750  cdlemk42  31752  dva1dim  31796  dia11N  31860  diaf11N  31861  cdlemm10N  31930  dib11N  31972  dibf11N  31973  diblsmopel  31983  dicffval  31986  dicfval  31987  dicopelval  31989  dicelvalN  31990  dicelval1sta  31999  cdlemn11pre  32022  dihord2pre  32037  dihffval  32042  dihfval  32043  dihlsscpre  32046  dihopelvalcpre  32060  dih11  32077  dihglblem5apreN  32103  dihmeetlem2N  32111  dihmeetlem4preN  32118  dihmeetlem13N  32131  dih1dimatlem0  32140  dih1dimatlem  32141  dihpN  32148  doch11  32185  dochsordN  32186  djhcvat42  32227  dihjatcclem4  32233  dvh3dim2  32260  dvh3dim3N  32261  islpolN  32295  lpolsatN  32300  lpolpolsatN  32301  lcfls1lem  32346  mapdffval  32438  mapdfval  32439  mapd11  32451  mapdsord  32467  mapdcnv11N  32471  mapdcv  32472  mapd0  32477  mapdpglem23  32506  mapdpg  32518  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524  mapdhval  32536  mapdheq  32540  mapdh9a  32602  hdmap1fval  32609  hdmap1vallem  32610  hdmap1val  32611  hdmap1eq  32614  hdmap1cbv  32615  hdmap11lem2  32657
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator