Theorem bitrd 278

Description: Deduction form of bitri 274. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.)

Hypotheses

Ref	Expression
bitrd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitrd.2	⊢ (𝜑 → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
bitrd	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitrd

Step	Hyp	Ref	Expression
1		bitrd.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	pm5.74i 270	. . 3 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
3		bitrd.2	. . . 4 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	3	pm5.74i 270	. . 3 ⊢ ((𝜑 → 𝜒) ↔ (𝜑 → 𝜃))
5	2, 4	bitri 274	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜃))
6	5	pm5.74ri 271	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bitr2d  279  bitr3d  280  bitr4d  281  bitrid  282  syl5bb  283  bitrdi  287  3bitrd  305  3bitr2d  307  3bitr3d  309  3bitr4d  311  imbi12d  345  bibi12d  346  sylan9bb  510  anbi12d  631  orbi12d  916  dedlem0a  1041  3bior2fd  1476  dral1v  2368  dral1vOLD  2369  dral1  2440  dral1ALT  2441  eleq12d  2834  reueqd  3351  rmoeqd  3352  raleqbid  3353  rexeqbid  3354  raleqbidva  3355  rexeqbidva  3356  ralxpxfr2d  3577  elabd2  3602  elabgt  3604  elabg  3608  eueq3  3647  reuxfrd  3684  reuxfr1d  3686  sbc19.21g  3795  sbcrext  3807  sbcabel  3812  sseq12d  3955  psseq12d  4030  sbceq1g  4349  sbceq2g  4351  sbcco3gw  4357  sbcco3g  4362  csbie2df  4375  2nreu  4376  raldifeq  4425  raaan  4452  raaanv  4453  elimhyp2v  4526  elimhyp4v  4528  keephyp2v  4532  ralsngf  4608  reusngf  4609  reuprg0  4639  reurexprg  4641  ssunsn2  4761  prel12g  4795  opthprneg  4796  2ralunsn  4827  disjeq12d  5049  disjprgw  5070  disjprg  5071  breq123d  5089  sbcbr1g  5132  sbcbr2g  5133  mpteq12da  5160  mpteq12dva  5164  treq  5198  nalset  5238  copsex4g  5410  opeqsng  5418  frirr  5567  posn  5673  sbcrel  5692  elrelimasn  5996  elinisegg  6004  epin  6006  brcodir  6029  dfpo2  6203  elpredg  6220  predep  6237  ordtri1  6303  sbcfung  6465  fneq12d  6537  feq12d  6597  feq123d  6598  sbcfng  6606  sbcfg  6607  f1osng  6766  dmfco  6873  eqfnfv2  6919  fvreseq1  6925  fndmdifeq0  6930  fneqeql2  6933  funimass3  6940  funconstss  6942  unpreima  6949  ralrnmptw  6979  ralrnmpt  6981  dffo3  6987  fmptco  7010  fressnfv  7041  fmptsnd  7050  fnunirn  7136  f1elima  7145  f12dfv  7154  f13dfv  7155  cocan1  7172  cocan2  7173  fliftf  7195  soisores  7207  isomin  7217  isoini  7218  f1oiso  7231  f1ofveu  7279  mpoeq123dva  7358  ovid  7423  ov  7426  ovg  7446  caovord2d  7490  ofrfval2  7563  offveqb  7567  elpwun  7628  ordpwsuc  7671  ordunisuc2  7700  tfindsg  7716  dfom2  7723  findsg  7755  f1oweALT  7824  reldm  7894  mposn  7952  suppval1  7992  fnsuppres  8016  fnsuppeq0  8017  suppssr  8021  mpoxopoveq  8044  mpoxopovel  8045  tpostpos  8071  mpocurryd  8094  csbfrecsg  8109  oe0m1  8360  oaord1  8391  omord  8408  omlimcl  8418  oewordi  8431  oeeui  8442  nnaordr  8460  nnaordex  8478  ereq1  8514  brdifun  8536  erth2  8557  elqsecl  8569  qliftfun  8600  brecop  8608  elmapg  8637  elpmg  8640  mapsnd  8683  ixpsnval  8697  boxcutc  8738  dom2lem  8789  xpcomco  8858  pw2f1olem  8872  nndomog  9008  nndomogOLD  9018  onomeneq  9020  unfilem2  9088  domunfican  9096  indexfi  9136  funisfsupp  9142  frnfsuppbi  9166  elfi2  9182  supisolem  9241  inflb  9257  hartogslem1  9310  brwdom2  9341  canthwdom  9347  infeq5i  9403  cantnfs  9433  cantnfp1lem3  9447  cantnfp1  9448  cantnflem1b  9453  cantnflem1  9456  cnfcom3lem  9470  ttrcltr  9483  r1pwALT  9613  rankxplim  9646  iscard2  9743  harsucnn  9765  infxpenc2  9787  fseqenlem1  9789  fseqdom  9791  alephnbtwn  9836  alephinit  9860  iunfictbso  9879  dfac2b  9895  dfac12lem2  9909  dfac12lem3  9910  kmlem2  9916  ackbij2lem2  10005  fin23lem23  10091  fin1a2lem2  10166  fin1a2lem4  10168  fin1a2lem9  10173  dcomex  10212  axdclem  10284  brdom7disj  10296  brdom6disj  10297  iundom2g  10305  axpownd  10366  fpwwe2lem8  10403  fpwwe2  10408  pwfseqlem1  10423  eltskm  10608  ltapi  10668  ltmpi  10669  nlt1pi  10671  indpi  10672  nqereu  10694  ordpipq  10707  ltsonq  10734  ltanq  10736  ltrnq  10744  archnq  10745  elnpi  10753  genpass  10774  addclprlem1  10781  mulclprlem  10784  1idpr  10794  prlem934  10798  prlem936  10812  reclem4pr  10815  addgt0sr  10869  sqgt0sr  10871  ltresr  10905  leloe  11070  eqlelt  11071  ltaddneg  11199  ltaddnegr  11200  negeu  11220  subadd2  11234  subcan2  11255  addrsub  11401  negn0  11413  ltadd1  11451  leadd2  11453  ltsubadd  11454  lesubadd  11456  ltaddsub2  11459  leaddsub2  11461  ltaddpos  11474  lesub2  11479  ltnegcon1  11485  ltnegcon2  11486  lenegcon1  11488  lenegcon2  11489  addge01  11494  addge02  11495  suble0  11498  leaddle0  11499  lesub0  11501  eqord2  11515  sublt0d  11610  mulcan2d  11618  mulcan2g  11638  diveq0  11652  diveq1  11675  rdiv  11819  lineq  11821  ltmul2  11835  lemul2  11837  ltmulgt11  11844  ltmulgt12  11845  gt0div  11850  ge0div  11851  mulle0b  11855  mulsuble0b  11856  ltmuldiv  11857  ltdiv2  11870  ltrec1  11871  lerec2  11872  ledivdiv  11873  ltdiv23  11875  lediv23  11876  creur  11976  creui  11977  ofsubeq0  11979  nn1suc  12004  nnrecl  12240  nn0sub  12292  frnnn0fsuppg  12301  znnsub  12375  zgt0ge1  12383  nn0le2is012  12393  btwnnz  12405  gtndiv  12406  eluz2  12597  uzwo  12660  indstr2  12676  rpneg  12771  divlt1lt  12808  divle1le  12809  nnledivrp  12851  xrleloe  12887  xnn0xadd0  12990  xltadd2  13000  xsubge0  13004  xlesubadd  13006  xmulasslem  13028  xlemul2  13034  xltmul2  13036  supxrre2  13074  elixx3g  13101  ioo0  13113  iccid  13133  ico0  13134  ioc0  13135  icc0  13136  elioc2  13151  elico2  13152  elicc2  13153  elfz2  13255  fzen  13282  fzsubel  13301  fzpr  13320  fzrevral2  13351  fzrevral3  13352  fzshftral  13353  nn0disj  13381  2ffzeq  13386  preduz  13387  fzosplitsni  13507  btwnzge0  13557  dfceil2  13568  mod0  13605  negmod0  13607  zmodidfzo  13629  nn0ennn  13708  rabssnn0fi  13715  expeq0  13822  sq11  13859  sq01  13949  hashen  14070  hashneq0  14088  hashnncl  14090  hashsdom  14105  hashunsnggt  14118  seqcoll2  14188  pr2pwpr  14202  hashge2el2dif  14203  hashge3el3dif  14209  csbwrdg  14256  wrdnval  14257  eqwrd  14269  ccat0  14289  ccats1alpha  14333  ccatws1lenp1b  14335  swrd0  14380  swrdspsleq  14387  pfxeq  14418  pfxsuffeqwrdeq  14420  pfxsuff1eqwrdeq  14421  ccatopth2  14439  wrd2ind  14445  s2eq2s1eq  14658  s2eq2seq  14659  s3eqs2s1eq  14660  s3eq3seq  14661  2swrd2eqwrdeq  14675  brcnvtrclfv  14723  cnpart  14960  sqrlem7  14969  sqrtneglem  14987  sqabs  15028  abslt  15035  absle  15036  absdiflt  15038  absdifle  15039  lenegsq  15041  rexfiuz  15068  rexanuz2  15070  limsupgle  15195  limsuple  15196  clim  15212  rlim  15213  clim0c  15225  rlim0  15226  rlim0lt  15227  ello12  15234  ello1mpt  15239  elo12  15245  lo1o12  15251  elo1mpt  15252  elo1mpt2  15253  o1lo1  15255  isercolllem2  15386  isercoll2  15389  zsum  15439  fsum2dlem  15491  binomlem  15550  zprod  15656  efieq  15881  sin01bnd  15903  cos01bnd  15904  dvdsval2  15975  modm1div  15984  modmulconst  16006  dvdsaddr  16021  dvdsabseq  16031  fzocongeq  16042  odd2np1  16059  oddp1d2  16076  zob  16077  oddm1d2  16078  nnoddm1d2  16104  divalglem4  16114  divalglem5  16115  divalgb  16122  modremain  16126  bits0  16144  bitsp1e  16148  bitsp1o  16149  bitscmp  16154  bitsinv1lem  16157  sadval  16172  sadcaddlem  16173  smuval  16197  smuval2  16198  dvdssq  16281  nn0seqcvgd  16284  algcvgblem  16291  lcmdvds  16322  lcmgcdeq  16326  coprmdvds  16367  qredeq  16371  congr  16378  isprm2  16396  isprm7  16422  prmdvdsexp  16429  prmdvdsexpb  16430  prmexpb  16434  prmfac1  16435  prmdvdsncoprmbd  16440  cncongrprm  16442  qnumgt0  16463  hashdvds  16485  fermltl  16494  modprminveq  16510  pcpremul  16553  pc2dvds  16589  pcz  16591  prmpwdvds  16614  prmreclem5  16630  4sqlem16  16670  vdwapun  16684  vdwmc  16688  vdwlem6  16696  ramval  16718  prmdvdsprmo  16752  prmgaplem7  16767  cshwsiun  16810  prdsbasmpt  17190  prdsleval  17197  prdsbasmpt2  17202  imasleval  17261  xpsle  17299  mrcidb2  17336  ismri  17349  mrieqvd  17356  acsfiel  17372  acsfn2  17381  catpropd  17427  ismon2  17455  isepi2  17462  isinv  17481  dfiso3  17494  invcoisoid  17513  isocoinvid  17514  cicsym  17525  isssc  17541  subsubc  17577  funcres2b  17621  funcpropd  17625  isfull  17635  isfth  17639  fullpropd  17645  isnat2  17673  fucsect  17699  fuciso  17702  isinito  17720  istermo  17721  initoeu2lem1  17738  elsetchom  17805  setcsect  17813  setciso  17815  elestrchom  17853  fullestrcsetc  17877  posi  18044  pltval3  18066  lubfval  18077  glbfval  18090  joindef  18103  meetdef  18117  tltnle  18149  latleeqj1  18178  latleeqj2  18179  latleeqm1  18194  latleeqm2  18195  ipodrsima  18268  isacs5  18275  acsficl2d  18279  mgm1  18351  gsumvalx  18369  gsumpropd  18371  gsumpropd2lem  18372  mhmpropd  18445  issubm2  18452  mndind  18475  elefmndbas2  18522  sgrp2rid2  18574  grpsubrcan  18665  grplactcnv  18687  grp1  18691  issubg  18764  eqgval  18814  conjnmzb  18878  isga  18906  gsmsymgrfixlem1  19044  f1omvdconj  19063  f1otrspeq  19064  pmtrmvd  19073  odmulg  19172  odf1o1  19186  odngen  19191  gexdvds  19198  pgpfi2  19220  isslw  19222  slwpss  19226  pgpssslw  19228  subgslw  19230  sylow2alem2  19232  fislw  19239  sylow3lem2  19242  lsmelvalm  19265  lsmdisj3a  19304  pj1eq  19315  iscmn  19403  eqgabl  19445  torsubg  19464  abl1  19476  gsumval3  19517  telgsums  19603  dprdf11  19635  dprd2da  19654  dmdprdpr  19661  ablfac1eulem  19684  pgpfac1lem2  19687  pgpfac1lem3a  19688  pgpfac1lem3  19689  srg1zr  19774  srgen1zr  19775  ringpropd  19830  dvdsrval  19896  dvdsr02  19907  unitpropd  19948  isrim  19986  drngmuleq0  20023  drngpropd  20027  issubrg  20033  islmod  20136  lsmelpr  20362  lspsnne1  20388  rngen1zr  20556  fidomndrnglem  20587  prmirredlem  20703  prmirred  20705  domnchr  20745  znleval  20771  znchr  20779  znunithash  20781  psgnevpmb  20801  iscss2  20900  ishil2  20935  dsmmelbas  20955  frlmplusgvalb  20985  frlmvscavalb  20986  frlmvplusgscavalb  20987  ellspd  21018  islindf  21028  islbs4  21048  islinds3  21050  coe1mul2lem2  21448  coe1tm  21453  gsumply1eq  21485  matbas2d  21581  mat1dimelbas  21629  scmatmats  21669  cramer0  21848  cpmatel2  21871  decpmataa0  21926  pm2mpf1  21957  fvmptnn04if  22007  chfacfscmul0  22016  chfacfpmmul0  22020  istopg  22053  eltg  22116  eltg2  22117  tgss2  22146  bastop1  22152  bastop2  22153  iscld  22187  iscld4  22225  elcls2  22234  elcls3  22243  isclo  22247  mretopd  22252  isnei  22263  neiint  22264  neindisj2  22283  islp2  22305  islp3  22306  maxlp  22307  cldlp  22310  neitr  22340  iscn  22395  iscnp  22397  iscnp3  22404  tgcn  22412  subbascn  22414  ssidcn  22415  lmbr2  22419  lmbrf  22420  cnnei  22442  cnrest2  22446  hausnei2  22513  cmpsub  22560  tgcmp  22561  cmpfi  22568  connsuba  22580  connsub  22581  dis2ndc  22620  subislly  22641  islocfin  22677  elkgen  22696  kgencn  22716  kgencn2  22717  eltx  22728  ptpjpre1  22731  ptcnplem  22781  hausdiag  22805  xkoptsub  22814  xkoco2cn  22818  imasnopn  22850  imasncld  22851  imasncls  22852  elqtop  22857  qtopcld  22873  kqcldsat  22893  kqt0lem  22896  isr0  22897  regr1lem2  22900  ordthmeolem  22961  ptuncnv  22967  trfbas  23004  elfg  23031  trfil3  23048  trufil  23070  filufint  23080  uffix2  23084  elfm2  23108  elfm3  23110  flimtopon  23130  flimopn  23135  fbflim  23136  fbflim2  23137  flffbas  23155  flftg  23156  cnflf  23162  txflf  23166  isfcls  23169  fclstopon  23172  fclsbas  23181  fclsrest  23184  fcfnei  23195  cnfcf  23202  ptcmplem2  23213  tgphaus  23277  tgpt0  23279  qustgphaus  23283  tsmsgsum  23299  tsmsres  23304  tsmsxplem1  23313  isust  23364  elutop  23394  utopsnneiplem  23408  utopsnnei  23410  isusp  23422  isucn  23439  isucn2  23440  ucncn  23446  ispsmet  23466  ismet  23485  isxmet  23486  metn0  23522  xmetres2  23523  elbl3ps  23553  elbl3  23554  xblpnfps  23557  xblpnf  23558  elmopn2  23607  metss  23673  stdbdxmet  23680  metcnp3  23705  metcnp  23706  metcnp2  23707  metcn  23708  txmetcnp  23712  txmetcn  23713  cfilucfil2  23726  blval2  23727  metuel  23729  metuel2  23730  metucn  23736  dscopn  23738  isngp3  23763  nmeq0  23783  ngppropd  23802  ngpocelbl  23877  isnghm3  23898  isnmhm2  23925  bl2ioo  23964  metdsge  24021  metnrmlem1a  24030  addcnlem  24036  elcncf  24061  elcncf2  24062  evth  24131  elpi1  24217  isclmp  24269  nmhmcn  24292  cphipeq0  24377  ipcau2  24407  lmmbr  24431  lmmbr2  24432  iscfil2  24439  fmcfil  24445  iscau2  24450  iscau3  24451  iscau4  24452  iscauf  24453  caucfil  24456  metcld2  24480  cfilucfil4  24494  bcthlem1  24497  lssbn  24525  cmetcusp1  24526  srabn  24533  ishl2  24543  rrxcph  24565  rrxplusgvscavalb  24568  rrxmet  24581  minveclem7  24608  ivth2  24628  ovolfioo  24640  ovolficc  24641  ovolshftlem1  24682  ovolicc2lem1  24690  icombl  24737  ioombl  24738  volsup2  24778  ismbf  24801  ismbfcn  24802  ismbfcn2  24811  mbfmax  24822  mbfimaopnlem  24828  mbfaddlem  24833  mbfsup  24837  mbfinf  24838  mbflimsup  24839  i1faddlem  24866  i1fres  24879  itg1ge0a  24885  itg1climres  24888  mbfi1fseqlem4  24892  itg2leub  24908  itg2const  24914  itg2split  24923  itg2cnlem2  24936  iblcnlem1  24961  iblrelem  24964  itgss3  24988  ellimc  25046  ellimc2  25050  ellimc3  25052  limcmpt  25056  limcmpt2  25057  limcres  25059  cnplimc  25060  limcun  25068  dvreslem  25082  dvcnp  25092  dvcnvlem  25149  dveflem  25152  cmvth  25164  mdegleb  25238  mdegldg  25240  degltp1le  25247  mdegle0  25251  deg1ldg  25266  coe1mul3  25273  ply1remlem  25336  fta1glem2  25340  ply1termlem  25373  coemulc  25425  coecj  25448  plymul0or  25450  ofmulrt  25451  quotval  25461  plydivlem4  25465  plyremlem  25473  ulmcau2  25564  reeff1o  25615  sincosq2sgn  25665  sinq12gt0  25673  coseq1  25690  logltb  25764  cosarg0d  25773  argrege0  25775  tanarg  25783  affineequiv  25982  affineequiv4  25985  affineequivne  25986  dcubic1lem  26002  dcubic  26005  atandm2  26036  rlimcnp  26124  rlimcnp2  26125  xrlimcnp  26127  fsumharmonic  26170  wilthlem1  26226  ftalem7  26237  basellem3  26241  isppw2  26273  issqf  26294  sqf11  26297  mumullem2  26338  sqff1o  26340  muinv  26351  ppiublem1  26359  vmasum  26373  chpchtsum  26376  chpub  26377  dchrelbas2  26394  dchrelbas3  26395  dchrelbas4  26400  dchrinv  26418  efexple  26438  bposlem1  26441  bposlem6  26446  bposlem7  26447  lgsdilem  26481  lgsdir2lem4  26485  lgsdir2  26487  lgsne0  26492  lgsabs1  26493  gausslemma2dlem3  26525  gausslemma2dlem7  26530  lgsquad3  26544  2lgslem1a  26548  2lgslem3c  26555  2lgslem3d  26556  2lgsoddprmlem4  26572  2sqlem7  26581  2sqlem8a  26582  2sq2  26590  2sqreulem1  26603  2sqreunnlem1  26606  chtppilim  26632  dchrvmaeq0  26661  dirith  26686  ostth3  26795  istrkgl  26828  iscgrglt  26884  tgcgr4  26901  legov  26955  legov2  26956  israg  27067  isperp  27082  opphllem3  27119  hpgbr  27130  lmiopp  27172  dfcgrg2  27233  xmstrkgc  27262  brbtwn  27276  brcgr  27277  eqeelen  27281  brbtwn2  27282  colinearalglem1  27283  colinearalglem2  27284  colinearalglem3  27285  colinearalg  27287  axcgrid  27293  ax5seglem4  27309  ax5seglem5  27310  axbtwnid  27316  axcontlem5  27345  axcontlem7  27347  ecgrtg  27360  uhgreq12g  27444  isuhgrop  27449  uhgr0e  27450  wrdupgr  27464  upgrop  27473  isumgrs  27475  wrdumgr  27476  uhgrvtxedgiedgb  27515  isusgrs  27535  isuspgrop  27540  isusgrop  27541  uhgr2edg  27584  issubgr2  27648  fusgrfisbase  27704  nbusgreledg  27729  usgrnbcnvfv  27741  nb3grprlem1  27756  uvtx2vtx1edgb  27775  iscplgrnb  27792  iscplgredg  27793  iscusgredg  27799  cplgr2vpr  27809  cusgr3vnbpr  27812  cusgrfilem3  27833  sizusglecusg  27839  vtxduhgr0edgnel  27870  vtxdgfusgrf  27873  1loopgrvd0  27880  umgr2v2enb1  27902  usgruvtxvdb  27905  vdiscusgrb  27906  isrgr  27935  isrusgr0  27942  rgrusgrprc  27965  isewlk  27978  iswlk  27986  upgriswlk  28017  wlkdlem1  28059  upgrf1istrl  28080  upgrwlkdvspth  28116  isspthonpth  28126  usgr2pth  28141  usgr2pth0  28142  iswwlksnx  28214  wlknewwlksn  28261  wlknwwlksnbij  28262  umgrwwlks2on  28331  wwlks2onsym  28332  usgr2wspthons3  28338  usgr2wspthon  28339  elwspths2spth  28341  rusgrnumwwlkl1  28342  clwlkclwwlklem2a4  28370  clwlkclwwlk  28375  clwlkclwwlk2  28376  clwwlkinwwlk  28413  clwwlkf  28420  clwwlkf1  28422  clwwlknwwlksnb  28428  eclclwwlkn1  28448  clwwlkvbij  28486  0clwlkv  28504  eupth2lem2  28592  eupth2lem3lem3  28603  eupth2lem3lem7  28607  isfrgr  28633  frgr3v  28648  frgrncvvdeqlem2  28673  fusgr2wsp2nb  28707  wlkl0  28740  isgrpo  28868  isablo  28917  vciOLD  28932  isvclem  28948  nmoubi  29143  nmobndi  29146  nmoo0  29162  isph  29193  minvecolem4b  29249  minvecolem4  29251  minvecolem5  29252  minvecolem7  29254  h2hcau  29350  h2hlm  29351  hvaddeq0  29440  hial2eq2  29478  norm-i  29500  hhssnv  29635  shsel  29685  shsel3  29686  pjhtheu2  29787  chssoc  29867  chsscon1  29872  chpsscon1  29875  chpsscon2  29876  chlejb2  29884  elspansn2  29938  fh1  29989  fh2  29990  cm2j  29991  eigposi  30207  nmopub  30279  unopf1o  30287  nmfnleub  30296  elnlfn  30299  adjvalval  30308  lnopcnre  30410  riesz4i  30434  leop2  30495  leop3  30496  leoppos  30497  hst1h  30598  mdbr2  30667  mdbr3  30668  mdbr4  30669  dmdbr2  30674  dmdbr3  30676  dmdbr4  30677  mddmd2  30680  cvdmd  30708  atcvatlem  30756  atdmd  30769  sumdmdii  30786  dmdbr5ati  30793  cdj3lem1  30805  addltmulALT  30817  opsbc2ie  30833  reuxfrdf  30848  eqrrabd  30858  iuneq12daf  30905  disjunsn  30942  br8d  30959  iunsnima2  30968  elimampt  30982  2ndimaxp  30993  abfmpeld  31000  abfmpel  31001  fmptcof2  31003  ressupprn  31033  f1od2  31065  suppss3  31068  fpwrelmapffslem  31076  xeqlelt  31106  nndiffz1  31116  hashgt1  31137  posrasymb  31252  isomnd  31336  ogrpinvlt  31358  isarchi  31445  isarchi3  31450  isarchiofld  31525  ecxpid  31565  rspsnel  31576  lindfpropd  31585  elgrplsmsn  31587  grplsm0l  31600  nsgqusf1olem3  31609  elrspunidl  31615  qsidomlem1  31637  extdg1id  31747  smatrcl  31755  1smat1  31763  ist0cld  31792  lmxrge0  31911  zrhker  31936  ismntop  31985  esumlub  32037  esum2dlem  32069  issiga  32089  dya2ub  32246  elcarsg  32281  itgeq12dv  32302  oddpwdc  32330  eulerpartlemgvv  32352  eulerpartlemgh  32354  orvcgteel  32443  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemrv1  32496  ballotlemrv2  32497  ballotlem1ri  32510  signswch  32549  reprpmtf1o  32615  reprdifc  32616  bnj1417  33030  bnj1452  33041  nummin  33072  derangval  33138  derangenlem  33142  subfacp1lem2a  33151  subfacp1lem5  33155  erdszelem8  33169  iccllysconn  33221  cvmsval  33237  goeleq12bg  33320  satfv1lem  33333  satfv1  33334  satfvsucsuc  33336  satfbrsuc  33337  fmlafvel  33356  satffunlem1lem2  33374  satffunlem2lem2  33377  sategoelfvb  33390  prv0  33401  prv1n  33402  untelirr  33658  untsucf  33660  untangtr  33664  onunel  33698  fv1stcnv  33760  fv2ndcnv  33761  dfon2lem3  33770  dfon2lem4  33771  dfon2lem7  33774  naddov2  33843  naddel2  33849  naddss2  33851  nosupbnd1lem3  33922  nosupbnd1lem5  33924  noinfbnd1lem3  33937  noetalem1  33953  eqscut2  34009  elold  34062  addscllem1  34140  cgrcomlr  34309  ifscgr  34355  cgr3permute2  34360  cgr3permute4  34361  cgr3permute5  34362  brcolinear2  34369  brcolinear  34370  colinearperm2  34375  colinearperm4  34376  colinearperm5  34377  brofs2  34388  brifs2  34389  btwnconn1lem3  34400  btwnconn1lem4  34401  btwnconn1lem5  34402  btwnconn1lem8  34405  btwnconn1lem10  34407  btwnconn1lem11  34408  brsegle2  34420  broutsideof3  34437  outsideofeu  34442  lineunray  34458  hfninf  34497  elicc3  34515  nn0prpwlem  34520  nn0prpw  34521  topfneec  34553  neibastop3  34560  neifg  34569  eltail  34572  filnetlem4  34579  nndivlub  34656  dnibndlem13  34679  unbdqndv1  34697  bj-pm11.53vw  34967  bj-equsalvwd  34971  bj-elgab  35136  bj-restuni  35277  copsex2d  35319  copsex2b  35320  opelopabbv  35323  brabd0  35327  bj-opelidres  35341  bj-idreseqb  35343  bj-elid4  35348  rdgeqoa  35550  csbfinxpg  35568  wl-ifp4impr  35647  curf  35764  uncf  35765  curunc  35768  finixpnum  35771  ltflcei  35774  lindsadd  35779  matunitlindf  35784  ptrest  35785  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem7  35793  poimirlem17  35803  poimirlem22  35808  poimirlem23  35809  poimirlem25  35811  poimirlem27  35813  poimirlem28  35814  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  poimir  35819  broucube  35820  itg2addnclem2  35838  itg2addnclem3  35839  itg2gt0cn  35841  itgaddnclem2  35845  iblabsnclem  35849  ftc1anclem1  35859  ftc1anclem5  35863  ftc1anclem7  35865  dvasin  35870  areacirclem1  35874  areacirclem4  35877  areacirclem5  35878  areacirc  35879  sdclem2  35909  lmclim2  35925  0totbnd  35940  sstotbnd  35942  isbnd3b  35952  ismtyval  35967  isismty  35968  ismtyima  35970  heiborlem7  35984  heiborlem10  35987  bfplem1  35989  rrnmet  35996  rrnheibor  36004  ismrer1  36005  ismgmOLD  36017  opidon2OLD  36021  ismndo1  36040  elghomlem2OLD  36053  rngosn3  36091  rngosn4  36092  isdrngo2  36125  iscom2  36162  isidlc  36182  eldmres2  36418  relcnveq2  36465  relcnveq4  36466  eldmcnv  36487  brxrn  36511  brin3  36543  br1cossres  36569  eldm1cossres  36585  brcosscnv  36597  elrelscnveq2  36618  elrelscnveq4  36619  brssrres  36629  elcoeleqvrelsrel  36716  brerser  36795  erim2  36796  eleldisjseldisj  36847  ax12el  36963  islshpsm  37001  lrelat  37035  islshpat  37038  islshpcv  37074  ellkr  37110  lkr0f  37115  lkrsc  37118  lshpkrlem1  37131  islshpkrN  37141  lfl1dim  37142  lkrpssN  37184  ldual1dim  37187  ople0  37208  opltn0  37211  op1le  37213  opcon2b  37218  oplecon1b  37222  opltcon1b  37226  opltcon2b  37227  cmtvalN  37232  omllaw4  37267  cmt4N  37273  cmtbr3N  37275  cmtbr4N  37276  omlfh1N  37279  cvrval  37290  pats  37306  leatb  37313  atlle0  37326  atlltn0  37327  cvlatcvr1  37362  cvlatcvr2  37363  ishlat1  37373  glbconxN  37399  hlsupr2  37408  hlateq  37420  hlrelat  37423  hlrelat2  37424  cvrval5  37436  cvrexchlem  37440  atcvr0eq  37447  cvrat4  37464  3dim0  37478  3dim2  37489  2dim  37491  islln3  37531  llnexatN  37542  islpln3  37554  islpln5  37556  islvol3  37597  islvol5  37600  4atlem11  37630  4atlem12  37633  lineset  37759  psubspset  37765  ispsubsp2  37767  elpmapat  37785  pmapglbx  37790  isline3  37797  isline4N  37798  elpaddat  37825  elpadd2at  37827  pmapjoin  37873  dalawlem13  37904  ispsubcl2N  37968  lhpoc  38035  lhpmod2i2  38059  lhpmod6i1  38060  lautset  38103  pautsetN  38119  ltrnatb  38158  ltrnel  38160  ltrncnvel  38163  ltrneq  38170  trlid0b  38199  cdleme0ex2N  38245  cdleme3  38258  cdleme7  38270  cdlemefrs29bpre0  38417  cdlemg2cN  38610  cdlemg2cex  38612  cdlemk34  38931  cdlemkid3N  38954  cdlemkid4  38955  cdlemk39s  38960  cdlemk42  38962  dvhb1dimN  39007  diaord  39068  dia11N  39069  diaglbN  39076  dia1dim2  39083  dvhopellsm  39138  dibelval3  39168  dibopelval3  39169  dibeldmN  39179  dib11N  39181  dib1dim  39186  diblsmopel  39192  diclspsn  39215  dihopelvalbN  39259  dihopelvalcqat  39267  dihopelvalcpre  39269  xihopellsmN  39275  dihopellsm  39276  dihord3  39278  dihord4  39279  dih11  39286  dihglbcpreN  39321  dihmeetlem4preN  39327  dihlspsnat  39354  dihatexv2  39360  dochord2N  39392  dochord3  39393  dochkrshp2  39408  dihjatcclem4  39442  dihjat1lem  39449  dvh2dimatN  39461  lcfl2  39514  lcfl3  39515  lcfl4N  39516  lcfl7N  39522  lcfrvalsnN  39562  lcfrlem9  39571  lcdlss  39640  mapdordlem2  39658  mapd1o  39669  mapdcv  39681  mapdn0  39690  mapdindp  39692  mapdpglem3  39696  mapdpglem26  39719  mapdpglem27  39720  mapdpglem30  39723  mapdindp1  39741  lspindp5  39791  hdmapeq0  39865  hdmap11  39869  hdmapoc  39952  hlhilphllem  39984  recbothd  40008  lcmineqlem4  40047  sticksstones1  40109  metakunt15  40146  metakunt16  40147  fsuppind  40286  fsuppssindlem2  40288  absdvdsabsb  40334  dvdsexpnn0  40348  renegeulemv  40358  sn-subeu  40415  sn-ltaddpos  40430  reposdif  40431  relt0neg2  40433  elrfi  40523  elrfirn2  40525  isnacs2  40535  mrefg3  40537  nacsfix  40541  lzunuz  40597  diophin  40601  sbc2rexgOLD  40617  sbc4rexgOLD  40619  4rexfrabdioph  40627  6rexfrabdioph  40628  diophren  40642  fiphp3d  40648  irrapxlem2  40652  elpell1qr2  40701  reglogltb  40720  reglogleb  40721  monotuz  40770  monotoddzz  40772  zindbi  40775  rmyeq0  40782  dvdsabsmod0  40816  jm2.19lem2  40819  jm2.19lem3  40820  rmydioph  40843  expdiophlem1  40850  expdioph  40852  pw2f1o2val2  40869  soeq12d  40870  freq12d  40871  weeq12d  40872  fnwe2lem2  40883  islmodfg  40901  islssfg2  40903  pwfi2f1o  40928  islnr3  40947  rngunsnply  41005  idomrootle  41027  iscard4  41147  minregex  41148  brfvrcld2  41307  brtrclfv2  41342  frege124d  41376  sbcheg  41394  frege72  41550  frege91  41569  frege92  41570  rfovcnvf1od  41619  fsovcnvlem  41628  uneqsn  41640  ntrk0kbimka  41656  ntrclselnel1  41674  ntrclsneine0lem  41681  ntrclsk2  41685  ntrclskb  41686  ntrclsk13  41688  ntrclsk4  41689  ntrneifv2  41697  ntrneineine0lem  41700  ntrneineine1lem  41701  ntrneicls00  41706  ntrneicls11  41707  ntrneiiso  41708  ntrneik2  41709  ntrneix2  41710  ntrneikb  41711  ntrneik3  41713  ntrneix3  41714  ntrneik13  41715  ntrneix13  41716  ntrneik4  41718  clsneiel1  41725  clsneiel2  41726  neicvgel2  41737  extoimad  41782  mnringelbased  41839  radcnvrat  41939  caofcan  41948  pm14.122c  42049  pm14.123c  42052  sbaniota  42060  trsbc  42167  fnchoice  42579  rfcnpre3  42583  rfcnpre4  42584  dffo3f  42724  fsneq  42753  elmptima  42811  supxrre3  42871  ltdivgt1  42902  ltdiv23neg  42941  supxrunb3  42946  supxrleubrnmpt  42953  suprleubrnmpt  42969  infxrunb3rnmpt  42975  uzub  42978  leneg2d  42995  infxrgelbrnmpt  43001  leneg3d  43004  supminfxr  43011  xlenegcon1  43034  xlenegcon2  43035  mccl  43146  climinf  43154  islptre  43167  climf  43170  islpcn  43187  clim0cf  43202  climresmpt  43207  climf2  43214  limsupref  43233  limsupbnd1f  43234  limsuppnfd  43250  climinf2  43255  limsuppnf  43259  climinfmpt  43263  limsupmnflem  43268  limsupmnf  43269  limsupre2lem  43272  limsupre2  43273  limsupmnfuzlem  43274  limsupmnfuz  43275  limsupre2mpt  43278  limsupre3lem  43280  limsupre3  43281  limsupre3mpt  43282  limsupre3uzlem  43283  limsupre3uz  43284  limsupreuz  43285  limsupreuzmpt  43287  climuz  43292  limsupge  43309  liminflelimsup  43324  limsupgt  43326  liminfreuzlem  43350  liminfreuz  43351  liminflt  43353  liminflimsupclim  43355  climliminflimsup2  43357  climliminflimsup3  43358  climliminflimsup4  43359  liminfpnfuz  43364  stoweidlem7  43555  stoweidlem27  43575  stoweidlem35  43583  fourierdlem71  43725  fourierdlem103  43757  fourierdlem104  43758  sge0lefimpt  43968  meadjiun  44011  meaiunincf  44028  meaiuninc3v  44029  caragenval  44038  caragenel  44040  omessle  44043  elhoi  44087  hoidmvlelem5  44144  hoidmvle  44145  ovnhoi  44148  ovolval5  44200  vonvolmbl2  44208  issmf  44273  issmff  44279  issmfle  44290  issmfgt  44301  issmfge  44315  smfrec  44334  smfmullem2  44337  smfmul  44340  smfsuplem2  44356  smfsup  44358  smfinflem  44361  smfinf  44362  confun  44445  fcoresf1  44574  f1cof1b  44580  fnfocofob  44582  focofob  44583  f1ocof1ob2  44585  dfdfat2  44631  fnbrafvb  44657  afvelrnb  44666  dmfcoafv  44678  dfatdmfcoafv2  44757  ltsubsubaddltsub  44804  readdcnnred  44806  resubcnnred  44807  cndivrenred  44809  2ffzoeq  44831  iccelpart  44896  iccpartnel  44901  fargshiftfva  44906  ich2exprop  44934  prproropreud  44972  prprelprb  44980  prprspr2  44981  poprelb  44987  fmtnof1  44998  odz2prm2pw  45026  flsqrt  45056  quad1  45083  requad1  45085  requad2  45086  oddm1evenALTV  45138  oddp1evenALTV  45139  mogoldbblem  45183  sbgoldbaltlem1  45242  nnsum3primesle9  45257  bgoldbtbnd  45272  isomushgr  45289  isomuspgr  45297  isupwlk  45309  upgrisupwlkALT  45315  mgmpropd  45340  mgmhmpropd  45350  issubmgm2  45355  0nodd  45375  isclintop  45412  isrnghm  45461  isrngim  45473  lidlmmgm  45494  uzlidlring  45498  rngcsect  45549  rngciso  45551  rngcsectALTV  45561  rngcisoALTV  45563  ringcsect  45600  ringciso  45602  ringcsectALTV  45624  ringcisoALTV  45626  pgrpgt2nabl  45713  lco0  45779  islinindfis  45801  islindeps  45805  lindslinindsimp1  45809  lindslinindsimp2  45815  lmod1  45844  divge1b  45864  divgt1b  45865  elbigo2  45909  logblt1b  45921  logbpw2m1  45924  nnpw2pmod  45940  rrx2plord2  46079  eenglngeehlnmlem2  46095  rrx2vlinest  46098  rrx2linest  46099  rrx2linest2  46101  line2  46109  line2xlem  46110  line2x  46111  line2y  46112  itsclc0yqsol  46121  itscnhlc0xyqsol  46122  itsclc0b  46129  itsclinecirc0b  46131  itsclinecirc0in  46132  itsclquadb  46133  itscnhlinecirc02p  46142  logic1  46147  opnneieqvv  46216  lubeldm2d  46263  glbeldm2d  46264  joindm3  46274  meetdm3  46276  ipolubdm  46284  ipoglbdm  46287  isthinc  46313  functhinc  46337  prstchom2  46370  grptcmon  46388  grptcepi  46389  aacllem  46516