Theorem syl5bb 282

Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)

Hypotheses

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

Assertion

Ref	Expression
syl5bb	⊢ (𝜒 → (𝜑 ↔ 𝜃))

Proof of Theorem syl5bb

Step	Hyp	Ref	Expression
1		syl5bb.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3		syl5bb.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	bitrd 278	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:  bitr2id  283  bitr3id  284  3bitr4g  313  imim21b  394  ifpfal  1073  norass  1535  cad0OLD  1622  ax12wdemo  2133  eu6lem  2573  abbi  2811  necon3abid  2979  necon3bid  2987  ceqsralv  3459  ralxpxfr2d  3568  ceqsrexv  3578  ceqsrex2v  3580  elabg  3600  elab2g  3604  elrabf  3613  elrab3t  3616  eueq2  3640  eqreu  3659  reu8  3663  ru  3710  sbc6g  3741  sbcieg  3751  sbcied  3756  sbcralt  3801  sbcabel  3807  ss2abdv  3993  rcompleq  4226  sbcel1g  4344  sbcel2  4346  csbnestgfw  4350  csbnestgf  4355  sbccsb2  4365  2nreu  4372  disjpss  4391  sbcssg  4451  2reu4lem  4453  rexsngf  4603  reusngf  4605  ralsng  4606  rexsng  4607  ralprgf  4625  rexprgf  4626  ralprg  4627  reuprg0  4635  difsn  4728  preq2b  4775  opthpr  4779  preqsnd  4786  csbopg  4819  ralunsn  4822  uniprg  4853  csbuni  4867  intprg  4909  dfiin2g  4958  iunxsng  5015  iunxsngf  5017  elpwuni  5030  disjxun  5068  sbcbr12g  5126  opthneg  5390  otthg  5394  copsex2g  5401  opeqsng  5411  snopeqop  5414  brsnop  5430  opelopabt  5438  opelopabga  5439  brabga  5440  opelopabgf  5446  csbmpt12  5463  rbropapd  5468  dfid3  5483  frirr  5557  wereu2  5577  opeliunxp  5645  posn  5663  sosn  5664  frsn  5665  brab2a  5670  opbrop  5674  csbcnvgALT  5782  dmopabelb  5814  elrnmpt1  5856  elrnmptg  5857  opelres  5886  eliniseg2  6003  poleloe  6025  xpdifid  6060  cnvpo  6179  reu3op  6184  elpredgg  6204  frpomin  6228  ordtri4  6288  oneqmini  6302  elsucg  6318  elsuc2g  6319  sbcfung  6442  dffun8  6446  fncnv  6491  fununi  6493  fnssresb  6538  fnimaeq0  6550  csbfv12  6799  dffn5  6810  funimass4  6816  feqmptdf  6821  fnsnfvOLD  6830  dmfco  6846  fndmdif  6901  fvimacnvi  6911  fvimacnvALT  6916  unpreima  6922  respreima  6925  fmptco  6983  fressnfv  7014  fmptsnd  7023  fnnfpeq0  7032  tpres  7058  elunirn  7106  dff13  7109  f12dfv  7126  f13dfv  7127  fliftel  7160  isoini  7189  f1oiso  7202  riotaeqimp  7239  fnbrovb  7304  eloprabga  7360  eloprabgaOLD  7361  resoprab2  7371  elrnmpores  7389  ralrnmpo  7390  ovid  7392  ov  7395  ovg  7415  ofrfval2  7532  dfwe2  7602  ssonprc  7614  ordpwsuc  7637  dfom2  7689  f1oweALT  7788  el2xptp0  7851  releldmdifi  7859  fmpox  7880  ovmptss  7904  1stconst  7911  2ndconst  7912  fnsuppres  7978  suppcoss  7994  brtpos2  8019  mpocurryd  8056  csbfrecsg  8071  dfsmo2  8149  rdglim2  8234  seqomlem2  8252  omeu  8378  oeeui  8395  brdifun  8485  eqerlem  8490  brecop  8557  erovlem  8560  eceqoveq  8569  mapfset  8596  mapsnd  8632  ixpsnval  8646  mptelixpg  8681  xpsnen  8796  xpdom2  8807  omxpenlem  8813  xpf1o  8875  mapunen  8882  onfin  8944  fimaxg  8991  fodomfib  9023  fofinf1o  9024  fipreima  9055  supub  9148  infglb  9179  infglbb  9180  fiming  9187  fiinfg  9188  ordtypecbv  9206  ordtypelem3  9209  ordtypelem9  9215  hartogslem1  9231  wofib  9234  wemapsolem  9239  wemapso2lem  9241  noinfep  9348  cantnf  9381  rankbnd2  9558  domtri2  9678  infxpenc2  9709  fseqdom  9713  acni2  9733  dfac9  9823  cfeq0  9943  cfsuc  9944  cflim3  9949  cfslb  9953  cofsmo  9956  enfin2i  10008  isfin3ds  10016  isf33lem  10053  fin1a2lem5  10091  axdc2lem  10135  zorn2g  10190  fodomb  10213  brdom7disj  10218  brdom6disj  10219  iundom2g  10227  cfpwsdom  10271  elgch  10309  fpwwe2cbv  10317  fpwwecbv  10331  pwfseqlem3  10347  pwfseqlem4a  10348  pwfseqlem4  10349  ltpiord  10574  nlt1pi  10593  nqereu  10616  addclprlem1  10703  1idpr  10716  reclem3pr  10736  ltsosr  10781  map2psrpr  10797  supsrlem  10798  axrrecex  10850  xrlenlt  10971  eqlei2  11016  addsubeq4  11166  renegcli  11212  lesub0  11422  wloglei  11437  conjmul  11622  rereccl  11623  infm3  11864  supaddc  11872  supadd  11873  supmul1  11874  supmullem1  11875  supmullem2  11876  supmul  11877  creui  11898  nndiv  11949  elznn0  12264  prime  12331  eqreznegel  12603  zsupss  12606  rebtwnz  12616  negelrp  12692  ltxr  12780  elixx3g  13021  ixxun  13024  ioo0  13033  ico0  13054  ioc0  13055  icc0  13056  difreicc  13145  divelunit  13155  iccf1o  13157  elfz2  13175  fzn  13201  fznn  13253  fzshftral  13273  nelfzo  13321  fzosplitsni  13426  om2uzisoi  13602  rabssnn0fi  13634  mptnn0fsupp  13645  sq11i  13836  hashsdom  14024  fi1uzind  14139  wrdval  14148  csbwrdg  14175  wrd2ind  14364  s2f1o  14557  cjreb  14762  rexfiuz  14987  cau3lem  14994  rlim2  15133  ello12  15153  ello1mpt  15158  elo12  15164  o1lo1  15174  lo1resb  15201  o1resb  15203  o1compt  15224  caucvgb  15319  mertens  15526  ruclem12  15878  divides  15893  dvdsabseq  15950  odd2np1  15978  oddm1even  15980  sumodd  16025  divalgmod  16043  modremain  16045  sadadd2lem2  16085  gcdcllem2  16135  bezoutlem2  16176  bezoutlem3  16177  bezoutlem4  16178  isprm2  16315  isprm3  16316  dvdsnprmd  16323  oddprmdvds  16532  prmreclem2  16546  prmreclem5  16549  prmreclem6  16550  4sqlem2  16578  4sqlem12  16585  vdwmc  16607  vdwpc  16609  vdwlem6  16615  vdwlem10  16619  vdwnn  16627  ramval  16637  0ram  16649  prdsleval  17105  pwsle  17120  imasleval  17169  xpsfrnel2  17192  xpsle  17207  isacs2  17279  mreacs  17284  acsfn  17285  iscatd2  17307  catpropd  17335  ciclcl  17431  cicrcl  17432  isssc  17449  evlfcl  17856  uncfcurf  17873  oduleg  17924  pltval  17965  lublecllem  17993  posglbmo  18045  tosso  18052  oduclatb  18140  odudlatb  18158  isipodrs  18170  gsumvalx  18275  elefmndbas  18427  sgrp2rid2  18480  grplmulf1o  18564  grplactcnv  18593  elnmz  18706  eqgid  18723  isghm  18749  ghmeqker  18776  resscntz  18853  symg1bas  18913  pgrpsubgsymgbi  18931  symgfixelq  18956  f1omvdconj  18969  odmulgeq  19079  sylow3lem3  19149  sylow3lem6  19152  efgval2  19245  efgsdm  19251  efgrelexlema  19270  efgcpbllemb  19276  iscyggen2  19396  cyggenod  19399  gsummptfzcl  19485  eldprd  19522  dprdf11  19541  dprddisj2  19557  pgpfac1lem2  19593  pgpfac1  19598  srg1zr  19680  drngid2  19922  issubrg  19939  sdrgacs  19984  islmod  20042  zndvds  20669  znleval  20674  iunocv  20798  pjfval2  20826  pjdm2  20828  dsmmelbas  20856  ellspd  20919  islindf  20929  islindf4  20955  aspval2  21012  psrbag  21030  cply1coe0bi  21381  istopg  21952  basgen2  22047  isclo  22146  mretopd  22151  isnei  22162  isperf3  22212  restdis  22237  neitr  22239  restcls  22240  restlp  22242  restperf  22243  iscn  22294  iscnp  22296  lmbr2  22318  lmbrf  22319  ordtt1  22438  cmpsub  22459  hauscmplem  22465  cmpfi  22467  dfconn2  22478  1stcelcls  22520  1stccn  22522  nllyi  22534  subislly  22540  dissnlocfin  22588  elkgen  22595  ptpjpre1  22630  ptuni2  22635  ptclsg  22674  ptcnplem  22680  txcn  22685  hausdiag  22704  txhaus  22706  txkgen  22711  xkoptsub  22713  cnmpt21  22730  elqtop  22756  tgqtop  22771  r0cld  22797  elfg  22930  fbasrn  22943  trfil2  22946  trfil3  22947  fin1aufil  22991  elfm2  23007  elfm3  23009  flimopn  23034  fbflim  23035  flfnei  23050  flftg  23055  cnpflf2  23059  txflf  23065  fclsbas  23080  alexsubALTlem4  23109  cnextfvval  23124  snclseqg  23175  tgphaus  23176  tsmsfbas  23187  tsmssubm  23202  utopsnneip  23308  prdsxmetlem  23429  imasdsf1olem  23434  xpsdsval  23442  blres  23492  isxms2  23509  metcnp  23603  txmetcnp  23609  txmetcn  23610  metustel  23612  metuel2  23627  dscopn  23635  isngp4  23674  cnblcld  23844  metnrmlem1a  23927  icoopnst  24008  iocopnst  24009  elpi1  24114  isclmp  24166  isncvsngp  24218  lmmbr2  24328  cfil3i  24338  caucfil  24352  iscmet3  24362  lmclim  24372  metcld2  24376  bcthlem4  24396  minveclem3b  24497  minveclem6  24503  minveclem7  24504  ivthle  24525  ivthle2  24526  evthicc2  24529  ovolfioo  24536  ovolficc  24537  ovolgelb  24549  dyadmax  24667  subopnmbl  24673  ismbf3d  24723  mbfimaopnlem  24724  mbfimaopn2  24726  mbfaddlem  24729  mbfsup  24733  mbfinf  24734  i1f1lem  24758  i1fmulclem  24772  itg1climres  24784  mbfi1fseqlem4  24788  itg2monolem1  24820  itg2gt0  24830  isibl  24835  iblcnlem1  24857  ellimc2  24946  dvcnvrelem1  25086  itgsubst  25118  mdegleb  25134  fta1glem2  25236  quotval  25357  vieta1lem1  25375  vieta1lem2  25376  ulm2  25449  ulmcaulem  25458  ulmcau  25459  radcnvlt1  25482  sineq0  25585  cos11  25594  recosf1o  25596  efopn  25718  cxpeq  25815  mcubic  25902  birthdaylem3  26008  rlimcnp  26020  xrlimcnp  26023  eldmgm  26076  dmgmaddn0  26077  lgamgulmlem6  26088  wilth  26125  isppw  26168  isppw2  26169  mumullem2  26234  sqff1o  26236  dvdsmulf1o  26248  fsumvma  26266  fsumvma2  26267  vmasum  26269  chpchtsum  26272  lgsne0  26388  gausslemma2dlem0i  26417  gausslemma2dlem1a  26418  lgseisenlem2  26429  lgsquadlem1  26433  lgsquadlem2  26434  2lgslem1a  26444  addsq2reu  26493  2sqreu  26509  2sqreunn  26510  2sqreult  26511  2sqreunnlt  26513  dchrmusumlema  26546  rpvmasum2  26565  dchrisum0lema  26567  pntibndlem3  26645  pntlemi  26657  pntleml  26664  pnt3  26665  trgcgrg  26780  tgcgr4  26796  colcom  26823  colrot1  26824  ltgov  26862  hlcomb  26868  lncom  26887  mirreu3  26919  isperp  26977  perpcom  26978  iscgra  27074  isinag  27103  brbtwn  27170  brcgr  27171  brbtwn2  27176  colinearalg  27181  axeuclidlem  27233  axcontlem2  27236  axcontlem4  27238  axcontlem7  27241  elntg2  27256  edgiedgb  27327  isuhgr  27333  isushgr  27334  isupgr  27357  isumgr  27368  isuspgr  27425  isusgr  27426  uhgr0v0e  27508  isfusgrf1  27590  opfusgr  27593  usgr1v0e  27596  dfnbgr3  27608  nbuhgr2vtx1edgb  27622  edgnbusgreu  27637  nbusgredgeu0  27638  isuvtx  27665  cusgruvtxb  27692  cplgr3v  27705  cusgrsizeinds  27722  vtxdg0v  27743  vtxd0nedgb  27758  vtxduhgr0nedg  27762  vtxdusgr0edgnelALT  27766  iswlk  27880  wlk1walk  27908  upgr2wlk  27938  upgristrl  27972  2pthnloop  28000  usgr2pthlem  28032  isclwlke  28046  isclwlkupgr  28047  iswwlksnx  28106  wwlksnextwrd  28163  wwlksnextproplem3  28177  2pthon3v  28209  umgr2wlk  28215  elwwlks2on  28225  elwwlks2  28232  elwspths2spth  28233  clwwlknclwwlkdif  28244  clwlkclwwlk  28267  clwlkclwwlk2  28268  clwwlkn1  28306  clwwlkn2  28309  clwwlkwwlksb  28319  eclclwwlkn1  28340  eleclclwwlkn  28341  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  clwwlknonel  28360  clwwlknon1  28362  clwwlknun  28377  1pthon2v  28418  uhgr3cyclex  28447  isconngr  28454  isconngr1  28455  eupthres  28480  eupth2lems  28503  frgr0v  28527  frgr3vlem2  28539  fusgr2wsp2nb  28599  extwwlkfab  28617  numclwwlk1lem2foa  28619  numclwwlk1lem2fo  28623  isvclem  28840  isnvlem  28873  isphg  29080  isph  29085  phoeqi  29120  ubthlem3  29135  minvecolem5  29144  minvecolem6  29145  minvecolem7  29146  hhph  29441  issh3  29482  nmopub  30171  nmfnleub  30188  adjeq  30198  adjvalval  30200  elunop2  30276  lnophm  30282  nmcexi  30289  cnlnadjlem5  30334  cnlnadjeui  30340  adjbd1o  30348  jpi  30533  mddmd2  30572  chrelati  30627  chrelat2i  30628  cvexchlem  30631  dmdbr5ati  30685  cdjreui  30695  cdj3i  30704  elunsn  30759  disjunsn  30834  opeldifid  30839  fcoinvbr  30848  brabgaf  30849  opabdm  30852  opabrn  30853  iunsnima  30859  nfpconfp  30868  elimampt  30874  abfmpunirn  30891  fmptcof2  30896  funcnvmpt  30906  funcnv5mpt  30907  suppiniseg  30922  ressupprn  30926  brprop  30932  f1od2  30958  resf1o  30967  fpwrelmap  30970  iocinioc2  31002  eliccioo  31107  wrdt2ind  31127  posrasymb  31145  mgccnv  31179  isslmd  31357  nsgqusf1olem3  31502  prmidl0  31528  fedgmullem2  31613  smatrcl  31648  rspectopn  31719  pstmxmet  31749  prsdm  31766  prsrn  31767  ordtconnlem1  31776  xrmulc1cn  31782  ispisys2  32021  elcarsg  32172  eulerpartlemmf  32242  isrrvv  32310  reprinrn  32498  tgoldbachgt  32543  bnj976  32657  bnj944  32818  bnj1173  32882  bnj1321  32907  bnj1373  32910  bnj1417  32921  fineqvrep  32964  lfuhgr  32979  revwlk  32986  usgrgt2cycl  32992  subfacp1lem3  33044  subfacp1lem6  33047  subfacp1  33048  txpconn  33094  sconnpi1  33101  resconn  33108  cvmscbv  33120  cvmsval  33128  cvmlift2lem13  33177  cvmlift3lem2  33182  cvmlift3  33190  goeleq12bg  33211  satfvsucsuc  33227  satfbrsuc  33228  fmlafvel  33247  satffunlem2lem1  33266  satefvfmla1  33287  mclsrcl  33423  fnssintima  33578  imaeqsexv  33593  br8  33629  br6  33630  br4  33631  elintfv  33644  fv1stcnv  33657  fv2ndcnv  33658  distel  33685  ttrclselem2  33712  ttrclse  33713  frxp2  33718  xpord2pred  33719  frxp3  33724  xpord3pred  33725  poseq  33729  wsuclem  33746  sltsolem1  33805  nosupdm  33834  nosupbnd1lem4  33841  slenlt  33882  sleloe  33884  eqscut2  33927  madeval2  33964  elold  33980  imageval  34159  funpartfv  34174  dfrdg4  34180  altopthg  34196  altopthbg  34197  brcolinear2  34287  lineext  34305  brsegle  34337  seglelin  34345  broutsideof2  34351  isfne4  34456  isfne2  34458  isfne3  34459  fneval  34468  topfneec  34471  neibastop2lem  34476  neibastop2  34477  neifg  34487  filnetlem4  34497  onsuct0  34557  bj-19.41t  34883  bj-sbievwd  34891  bj-elgab  35054  bj-tagcg  35102  bj-projval  35113  bj-restuni  35195  opelopabd  35239  opelopabb  35240  brabd0  35245  bj-opelid  35254  bj-ideqg  35255  bj-opelidres  35259  bj-ideqg1  35262  bj-elid6  35268  bj-isvec  35385  bj-isclm  35389  bj-isrvecd  35396  csboprabg  35428  csbmpo123  35429  topdifinffinlem  35445  isbasisrelowllem1  35453  isbasisrelowllem2  35454  rdgeqoa  35468  csbfinxpg  35486  nlpineqsn  35506  wl-3xortru  35569  wl-3xorfal  35570  wl-sbrimt  35632  wl-sblimt  35633  wl-sbnf1  35637  wl-mo2df  35652  wl-eudf  35654  wl-mo2t  35657  wl-mo3t  35658  wl-ax11-lem6  35668  wl-dfclab  35674  uncov  35685  tan2h  35696  matunitlindf  35702  ptrest  35703  poimirlem2  35706  poimirlem16  35720  poimirlem19  35723  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  mbfposadd  35751  cnambfre  35752  itg2addnclem2  35756  fdc  35830  heibor1  35895  rrncmslem  35917  rrnheibor  35922  opidonOLD  35937  issmgrpOLD  35948  ismndo  35957  isrngo  35982  isdivrngo  36035  isfldidl2  36154  isdmn3  36159  releleccnv  36323  releccnveq  36324  brcnvep  36331  elecres  36339  eleccnvep  36343  ideq2  36370  extid  36373  relcnveq3  36383  eqres  36402  brrabga  36403  ecin0  36411  alrmomodm  36418  brxrn  36431  brxrn2  36432  elecxrn  36443  br1cnvxrn2  36449  elec1cnvxrn2  36450  br1cossinres  36492  br1cossxrnres  36493  eldmcoss  36503  elrels2  36531  elrelscnveq3  36536  br1cnvssrres  36550  brcnvssr  36551  dfrefrels2  36558  dfcnvrefrels2  36571  dfsymrels2  36586  elrefsymrelsrel  36612  dftrrels2  36616  erim2  36716  eldisjs5  36764  prtlem13  36809  prter3  36823  lrelat  36955  islshpat  36958  lshpsmreu  37050  lkrpssN  37104  cmtvalN  37152  omllaw2N  37185  cvrval  37210  cvrval2  37215  cvlsupr3  37285  3dim0  37398  islln2  37452  islpln5  37476  islpln2  37477  islpln2ah  37490  islvol5  37520  islvol2  37521  4atlem11  37550  pmapglbx  37710  cdleme18d  38236  cdlemefrs29bpre0  38337  cdlemb3  38547  cdlemg33b  38648  cdlemkid3N  38874  cdlemkid4  38875  dvhb1dimN  38927  dia11N  38989  cdlemm10N  39059  dib11N  39101  dib1dim  39106  dibglbN  39107  diblsmopel  39112  dihopelvalcpre  39189  dih11  39206  dihmeetlem4preN  39247  dihmeetlem13N  39260  lcfrvalsnN  39482  lcfrlem9  39491  lcf1o  39492  mapdval4N  39573  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  hdmap1fval  39737  hdmapfval  39768  hdmapglem7a  39868  hlhillcs  39903  elab2gw  40094  19.9dev  40106  frlmfielbas  40157  fsuppind  40202  fsuppssindlem2  40204  addsubeq4com  40229  prjspreln0  40369  ellz1  40505  lzunuz  40506  fz1eqin  40507  diophrex  40513  rexrabdioph  40532  rexfrabdioph  40533  2rexfrabdioph  40534  3rexfrabdioph  40535  4rexfrabdioph  40536  6rexfrabdioph  40537  7rexfrabdioph  40538  fzneg  40720  expdioph  40761  wepwsolem  40783  fnwe2lem2  40792  islmodfg  40810  kercvrlsm  40824  cnvcnvintabd  41097  sqrtcvallem1  41128  iunrelexpuztr  41216  brtrclfv2  41224  frege124d  41258  or3or  41520  uneqsn  41522  clsk1independent  41545  ntrclsneine0lem  41563  ntrclsiso  41566  ntrclsk2  41567  ntrclskb  41568  ntrclsk3  41569  ntrclsk13  41570  ntrclsk4  41571  ntrneiel2  41585  ntrneiiso  41590  ntrneikb  41593  ntrneik3  41595  ntrneix3  41596  ntrneik13  41597  ntrneix13  41598  ntrneik4w  41599  k0004lem3  41648  scottabf  41747  pm10.52  41872  iotasbc  41926  pm14.122a  41929  pm14.122b  41930  pm14.123a  41932  rusbcALT  41946  fvsb  41959  trsbc  42049  wessf1ornlem  42611  imassmpt  42699  limcperiod  43059  limsupre  43072  dvbdfbdioo  43361  stoweidlem34  43465  fourierdlem108  43645  fourierdlem110  43647  etransc  43714  funressnfv  44424  dfafn5a  44539  ndfatafv2nrn  44600  afv2ndefb  44603  dfatsnafv2  44631  dfatdmfcoafv2  44633  dfatco  44635  afv2fv0xorb  44646  readdcnnred  44683  resubcnnred  44684  recnmulnred  44685  cndivrenred  44686  elfz2z  44695  el1fzopredsuc  44705  elsetpreimafvb  44724  iccelpart  44773  ichan  44795  ichal  44806  reupr  44862  lighneallem2  44946  dfeven2  44989  gbowge7  45103  sbgoldbwt  45117  isupwlk  45186  uspgrsprfo  45198  ismhm0  45247  inclfusubc  45313  isrnghm  45338  rnghmval2  45341  uzlidlring  45375  lidldomnnring  45376  zrninitoringc  45517  opeliun2xp  45556  snlindsntor  45700  elbigo2  45786  resum2sqorgt0  45943  rrx2pnedifcoorneor  45950  rrx2plord  45954  rrx2plordisom  45957  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  rrx2linest2  45978  itsclc0b  46006  itsclinecirc0in  46009  inlinecirc02plem  46020  fvconstr  46071  fvconstrn0  46072  opndisj  46084  clddisj  46085  i0oii  46101  io1ii  46102  isthincd2lem1  46196  functhinc  46214  gte-lte  46312  gt-lt  46313