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

Theorem bitrd 246
Description: Deduction form of bitri 242. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.)
Hypotheses
Ref Expression
bitrd.1  |-  ( ph  ->  ( ps  <->  ch )
)
bitrd.2  |-  ( ph  ->  ( ch  <->  th )
)
Assertion
Ref Expression
bitrd  |-  ( ph  ->  ( ps  <->  th )
)

Proof of Theorem bitrd
StepHypRef Expression
1 bitrd.1 . . . 4  |-  ( ph  ->  ( ps  <->  ch )
)
21pm5.74i 238 . . 3  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
3 bitrd.2 . . . 4  |-  ( ph  ->  ( ch  <->  th )
)
43pm5.74i 238 . . 3  |-  ( (
ph  ->  ch )  <->  ( ph  ->  th ) )
52, 4bitri 242 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  th ) )
65pm5.74ri 239 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  bitr2d  247  bitr3d  248  bitr4d  249  syl5bb  250  syl6bb  254  3bitrd  272  3bitr2d  274  3bitr3d  276  3bitr4d  278  imbi12d  313  bibi12d  314  sylan9bb  682  orbi12d  692  anbi12d  693  dedlem0a  920  ax11el  2134  eleq12d  2352  neeq12d  2462  raleqbi1dv  2745  rexeqbi1dv  2746  reueqd  2747  rmoeqd  2748  raleqbidv  2749  rexeqbidv  2750  raleqbidva  2751  rexeqbidva  2752  eueq3  2941  sbc19.21g  3056  sbcrext  3065  sbcabel  3069  sbcel1g  3101  sbceq1g  3102  sbcel2g  3103  sbceq2g  3104  sbccsb2g  3111  sbcco3g  3137  sseq12d  3208  psseq12d  3271  raaan  3562  raaanv  3563  sbcss  3565  elimhyp2v  3615  elimhyp4v  3617  keephyp2v  3621  ralsng  3673  rexsng  3674  ssunsn2  3774  2ralunsn  3817  csbunig  3836  disjeq12d  4003  disjprg  4020  breq123d  4038  sbcbr12g  4074  sbcbr1g  4075  sbcbr2g  4076  treq  4120  nalset  4152  copsex4g  4254  frirr  4369  ordtri1  4424  reusv7OLD  4545  reuxfr2d  4556  reuxfrd  4558  elpwun  4566  ordpwsuc  4605  ordunisuc2  4634  tfindsg  4650  dfom2  4657  findsg  4682  csbxpg  4715  posn  4757  frsn  4759  csbrng  4922  elrelimasn  5036  eliniseg  5041  brcodir  5061  fneq12d  5302  feq12d  5346  feq123d  5347  f1osng  5479  f1oprswap  5480  fv2  5481  csbfv12g  5495  csbfv12gALT  5496  dmfco  5554  eqfnfv2  5584  fndmdifeq0  5592  fneqeql2  5595  funimass3  5602  funconstss  5604  unpreima  5612  ralrnmpt  5630  dffo3  5636  fmptco  5652  fressnfv  5668  fnsuppeq0  5694  fnunirn  5739  f1elima  5748  cocan1  5762  cocan2  5763  fliftf  5775  soisores  5785  isomin  5795  isoini  5796  f1oiso  5809  f1oweALT  5812  mpt2eq123dva  5870  ovid  5925  ov  5928  ovg  5947  caovord2d  5990  ofrfval2  6057  offveqb  6060  reldm  6132  tpostpos  6215  f1ofveu  6334  oe0m1  6515  oaord1  6544  omord  6561  omlimcl  6571  oewordi  6584  oeeui  6595  nnaordr  6613  nnaordex  6631  ereq1  6662  brdifun  6682  erth2  6700  qliftfun  6738  brecop  6746  elmapg  6780  elpmg  6781  boxcutc  6854  dom2lem  6896  xpcomco  6947  pw2f1olem  6961  nndomo  7049  unfilem2  7117  domunfican  7124  indexfi  7158  elfi2  7163  supisolem  7216  hartogslem1  7252  brwdom2  7282  canthwdom  7288  infeq5i  7332  cantnfs  7362  cantnfrescl  7373  cantnfp1lem3  7377  cantnflem1b  7383  cantnflem1  7386  cnfcom3lem  7401  r1pwOLD  7513  rankxplim  7544  iscard2  7604  infxpenc2  7644  fseqenlem1  7646  fseqdom  7648  alephnbtwn  7693  alephinit  7717  iunfictbso  7736  dfac2  7752  dfac12lem2  7765  dfac12lem3  7766  kmlem2  7772  ackbij2lem2  7861  fin23lem23  7947  fin1a2lem2  8022  fin1a2lem4  8024  fin1a2lem9  8029  dcomex  8068  axdclem  8141  brdom7disj  8151  brdom6disj  8152  iundom2g  8157  axpownd  8218  fpwwe2cbv  8247  fpwwe2lem2  8249  fpwwe2lem3  8250  fpwwe2lem9  8255  fpwwe2  8260  pwfseqlem1  8275  eltskm  8460  ltapi  8522  ltmpi  8523  nlt1pi  8525  indpi  8526  nqereu  8548  ordpipq  8561  ltsonq  8588  ltanq  8590  ltrnq  8598  archnq  8599  elnpi  8607  genpass  8628  addclprlem1  8635  mulclprlem  8638  1idpr  8648  prlem934  8652  prlem936  8666  reclem4pr  8669  addgt0sr  8721  sqgt0sr  8723  ltresr  8757  leloe  8903  eqlelt  8904  negeu  9037  subadd2  9050  subcan2  9067  ltadd1  9236  leadd2  9238  ltsubadd  9239  lesubadd  9241  ltaddsub2  9244  leaddsub2  9246  ltaddpos  9259  lesub2  9264  ltnegcon1  9270  ltnegcon2  9271  lenegcon1  9273  lenegcon2  9274  addge01  9279  addge02  9280  suble0  9283  lesub0  9285  eqord2  9299  mulcan2d  9397  diveq0  9429  diveq1  9449  ltmul2  9602  lemul2  9604  ltmulgt11  9611  ltmulgt12  9612  gt0div  9617  ge0div  9618  ltmuldiv  9621  ledivmul2OLD  9629  ltdiv2  9636  ltrec1  9638  lerec2  9639  ledivdiv  9640  ltdiv23  9642  lediv23  9643  creur  9735  creui  9736  ofsubeq0  9738  nn1suc  9762  nnrecl  9958  nn0sub  10009  znnsub  10059  btwnnz  10083  gtndiv  10084  uzindOLD  10101  eluz2  10231  uzwo  10276  uzwoOLD  10277  indstr2  10291  negn0  10299  rpneg  10378  xrleloe  10473  xltadd2  10571  xsubge0  10575  xlesubadd  10577  xmulasslem  10599  xlemul2  10605  xltmul2  10607  supxrre2  10644  elixx3g  10663  ioo0  10675  iccid  10695  ico0  10696  ioc0  10697  icc0  10698  elioc2  10707  elico2  10708  elicc2  10709  elfz2  10783  fzen  10805  fzsubel  10821  fzpr  10834  fzrevral2  10861  fzrevral3  10862  fzshftral  10863  fzosplitsni  10915  btwnzge0  10947  mod0  10972  negmod0  10973  nn0ennn  11035  expeq0  11126  sq11  11170  sq01  11217  hashen  11340  hashnncl  11348  hashsdom  11357  seqcoll2  11396  ccatopth2  11457  cnpart  11719  sqrlem7  11728  sqrneglem  11746  sqabs  11786  abslt  11792  absle  11793  absdiflt  11795  absdifle  11796  lenegsq  11798  rexanuz2  11827  limsupgle  11945  limsuple  11946  clim  11962  rlim  11963  clim0c  11975  rlim0  11976  rlim0lt  11977  ello12  11984  ello1mpt  11989  elo12  11995  lo1o12  12001  elo1mpt  12002  elo1mpt2  12003  o1lo1  12005  isercolllem2  12133  isercoll2  12136  zsum  12185  fsum2dlem  12227  fsumcom2  12231  binomlem  12281  efieq  12437  sin01bnd  12459  cos01bnd  12460  dvdsval2  12528  dvdsaddr  12562  fzocongeq  12576  odd2np1  12581  divalglem4  12589  divalglem5  12590  divalgb  12597  bits0  12613  bitsp1e  12617  bitsp1o  12618  bitscmp  12623  bitsinv1lem  12626  sadval  12641  sadcaddlem  12642  smuval  12666  smuval2  12667  dvdssq  12733  nn0seqcvgd  12734  algcvgblem  12741  isprm2  12760  qredeq  12779  prmdvdsexp  12787  prmdvdsexpb  12788  prmexpb  12790  prmfac1  12791  qnumgt0  12815  hashdvds  12837  fermltl  12846  pcpremul  12890  pc2dvds  12925  pcz  12927  prmpwdvds  12945  prmreclem5  12961  4sqlem16  13001  vdwapun  13015  vdwmc  13019  vdwlem6  13027  ramval  13049  prdsbasmpt  13363  prdsleval  13370  prdsbasmpt2  13375  imasleval  13437  xpsle  13477  mrcidb2  13514  ismri  13527  mrieqvd  13534  acsfiel  13550  acsfn2  13559  catpropd  13606  cidpropd  13607  ismon2  13631  isepi2  13638  isinv  13656  isssc  13691  subsubc  13721  funcres2b  13765  funcpropd  13768  isfull  13778  isfth  13782  fullpropd  13788  isnat2  13816  fucsect  13840  fuciso  13843  elsetchom  13907  setcsect  13915  setciso  13917  evlfcl  13990  isprs  14058  isdrs  14062  posi  14078  pltval3  14095  istos  14135  islat  14147  latleeqj1  14163  latleeqj2  14164  latleeqm1  14179  latleeqm2  14180  ipodrsima  14262  isacs5  14269  acsficl2d  14273  isdlat  14290  ismgmid  14381  mhmpropd  14415  issubm2  14420  gsumvalx  14445  gsumpropd  14447  grpsubrcan  14541  grplactcnv  14558  issubg  14615  eqgval  14660  conjnmzb  14711  isga  14739  odmulg  14863  odf1o1  14877  odngen  14882  gexdvds  14889  pgpfi2  14911  isslw  14913  slwpss  14917  pgpssslw  14919  subgslw  14921  sylow2alem2  14923  fislw  14930  sylow3lem2  14933  lsmelvalm  14956  lsmdisj3a  14992  pj1eq  15003  iscmn  15090  eqgabl  15125  torsubg  15140  gsumval3  15185  dprdf11  15252  dprd2da  15271  dmdprdpr  15278  ablfac1eulem  15301  pgpfac1lem2  15304  pgpfac1lem3a  15305  pgpfac1lem3  15306  rngpropd  15366  dvdsrval  15421  dvdsr02  15432  unitpropd  15473  drngmuleq0  15529  drngpropd  15533  issubrg  15539  islmod  15625  lsmelpr  15838  lspsnne1  15864  fidomndrnglem  16041  coe1mul2lem2  16339  coe1tm  16343  prmirredlem  16440  prmirred  16442  domnchr  16480  znleval  16502  znchr  16510  znunithash  16512  iscss2  16580  ishil2  16613  istopg  16635  eltg  16689  eltg2  16690  tgss2  16719  bastop1  16725  bastop2  16726  iscld  16758  iscld4  16796  elcls2  16805  elcls3  16814  isclo  16818  mretopd  16823  isnei  16834  neiint  16835  neindisj2  16854  islp2  16871  maxlp  16872  cldlp  16875  iscn  16959  iscnp  16961  iscnp3  16968  tgcn  16976  subbascn  16978  ssidcn  16979  lmbr2  16983  lmbrf  16984  cnrest2  17008  hausnei2  17075  cmpsub  17121  tgcmp  17122  cmpfi  17129  consuba  17140  connsub  17141  dis2ndc  17180  subislly  17201  elkgen  17225  kgencn  17245  kgencn2  17246  eltx  17257  ptpjpre1  17260  ptcnplem  17309  hausdiag  17333  xkoptsub  17342  xkoco2cn  17346  elqtop  17382  qtopcld  17398  kqcldsat  17418  kqt0lem  17421  isr0  17422  regr1lem2  17425  ordthmeolem  17486  ptuncnv  17492  trfbas  17533  elfg  17560  trfil3  17577  trufil  17599  filufint  17609  uffix2  17613  elfm2  17637  elfm3  17639  flimtopon  17659  flimopn  17664  fbflim  17665  fbflim2  17666  flffbas  17684  flftg  17685  cnflf  17691  txflf  17695  isfcls  17698  fclstopon  17701  fclsbas  17710  fclsrest  17713  fcfnei  17724  cnfcf  17731  ptcmplem2  17741  tgphaus  17793  tgpt0  17795  divstgphaus  17799  tsmsgsum  17815  tsmsres  17820  tsmsxplem1  17829  ismet  17882  isxmet  17883  metn0  17918  xmetres2  17919  elbl3  17945  xblpnf  17947  elmopn2  17985  metss  18048  stdbdxmet  18055  metcnp3  18080  metcnp  18081  metcnp2  18082  metcn  18083  txmetcnp  18087  txmetcn  18088  dscopn  18090  isngp3  18114  nmeq0  18133  ngppropd  18147  isnghm3  18228  isnmhm2  18255  bl2ioo  18292  metdsge  18347  metnrmlem1a  18356  addcnlem  18362  elcncf  18387  elcncf2  18388  evth  18451  elpi1  18537  nmhmcn  18595  cphipeq0  18633  ipcau2  18658  lmmbr  18678  lmmbr2  18679  iscfil2  18686  fmcfil  18692  iscau  18696  iscau2  18697  iscau3  18698  iscau4  18699  iscauf  18700  caucfil  18703  metcld2  18726  bcthlem1  18740  lssbn  18767  srabn  18771  ishl2  18781  minveclem7  18793  ivth2  18809  ovolfioo  18821  ovolficc  18822  ovolshftlem1  18862  ovolicc2lem1  18870  icombl  18915  ioombl  18916  volsup2  18954  ismbf  18979  ismbfcn  18980  ismbfcn2  18988  mbfmax  18998  mbfimaopnlem  19004  mbfaddlem  19009  mbfsup  19013  mbfinf  19014  mbflimsup  19015  i1faddlem  19042  i1fres  19054  itg1ge0a  19060  itg1climres  19063  mbfi1fseqlem4  19067  itg2leub  19083  itg2const  19089  itg2split  19098  itg2cnlem2  19111  iblcnlem1  19136  iblrelem  19139  itgss3  19163  ellimc  19217  ellimc2  19221  ellimc3  19223  limcmpt  19227  limcmpt2  19228  limcres  19230  cnplimc  19231  limcun  19239  dvreslem  19253  dvcnp  19262  dvcnvlem  19317  dveflem  19320  cmvth  19332  mdegleb  19444  mdegldg  19446  degltp1le  19453  mdegle0  19457  deg1ldg  19472  coe1mul3  19479  ply1remlem  19542  fta1glem2  19546  ply1termlem  19579  coemulc  19630  coecj  19653  plymul0or  19655  ofmulrt  19656  quotval  19666  plydivlem4  19670  plyremlem  19678  ulmcau2  19767  reeff1o  19817  sincosq2sgn  19861  sinq12gt0  19869  coseq1  19884  logltb  19947  cosarg0d  19957  argrege0  19959  tanarg  19964  affineequiv  20117  dcubic1lem  20133  dcubic  20136  atandm2  20167  rlimcnp  20254  rlimcnp2  20255  xrlimcnp  20257  fsumharmonic  20299  wilthlem1  20300  ftalem7  20310  basellem3  20314  isppw2  20347  issqf  20368  sqf11  20371  mumullem2  20412  sqff1o  20414  muinv  20427  ppiublem1  20435  vmasum  20449  chpchtsum  20452  chpub  20453  dchrelbas2  20470  dchrelbas3  20471  dchrelbas4  20476  dchrinv  20494  efexple  20514  bposlem1  20517  bposlem6  20522  bposlem7  20523  lgsdilem  20555  lgsdir2lem4  20559  lgsdir2  20561  lgsne0  20566  lgsabs1  20567  lgsquad3  20594  2sqlem7  20603  2sqlem8a  20604  chtppilim  20618  dchrvmaeq0  20647  dirith  20672  ostth3  20781  isgrpo  20855  isablo  20942  ismgm  20979  opidon2  20983  ismndo1  21003  elghomlem2  21021  isrngo  21037  iscom2  21071  rngosn3  21085  rngosn4  21086  vci  21096  isvclem  21125  vcoprnelem  21126  nvsubadd  21205  nvelbl  21254  nvelbl2  21255  nmoubi  21342  nmobndi  21345  nmoo0  21361  isph  21392  minvecolem4b  21449  minvecolem4  21451  minvecolem5  21452  minvecolem7  21454  h2hcau  21551  h2hlm  21552  hvaddeq0  21640  hial2eq2  21678  norm-i  21700  hhssnv  21833  shsel  21885  shsel3  21886  pjhtheu2  21987  chssoc  22067  chsscon1  22072  chpsscon1  22075  chpsscon2  22076  chlejb2  22084  elspansn2  22138  fh1  22189  fh2  22190  cm2j  22191  eigposi  22408  nmopub  22480  unopf1o  22488  nmfnleub  22497  elnlfn  22500  adjvalval  22509  lnopcnre  22611  riesz4i  22635  leop2  22696  leop3  22697  leoppos  22698  hst1h  22799  mdbr2  22868  mdbr3  22869  mdbr4  22870  dmdbr2  22875  dmdbr3  22877  dmdbr4  22878  mddmd2  22881  cvdmd  22909  atcvatlem  22957  atdmd  22970  sumdmdii  22987  dmdbr5ati  22994  cdj3lem1  23006  addltmulALT  23018  ballotlemfc0  23044  ballotlemfcc  23045  ballotlemrv  23071  ballotlemrv1  23072  ballotlemrv2  23073  ballotlem1ri  23086  derangval  23102  derangenlem  23106  subfacp1lem2a  23115  subfacp1lem5  23119  erdszelem8  23133  iccllyscon  23185  cvmsval  23201  isumgra  23271  wrdumgra  23272  iseupa  23285  eupath2lem2  23306  eupath2lem3  23307  untelirr  23458  untsucf  23460  untangtr  23464  mulcan2g  23488  mulle0b  23490  mulsuble0b  23491  dfpo2  23515  dfon2lem3  23542  dfon2lem4  23543  dfon2lem7  23546  elpredim  23577  predep  23593  preduz  23601  brbtwn  23934  brcgr  23935  eqeelen  23939  brbtwn2  23940  colinearalglem1  23941  colinearalglem2  23942  colinearalglem3  23943  colinearalg  23945  axcgrid  23951  ax5seglem4  23967  ax5seglem5  23968  axbtwnid  23974  axcontlem5  24003  axcontlem7  24005  cgrcomlr  24028  ifscgr  24074  cgr3permute2  24079  cgr3permute4  24080  cgr3permute5  24081  brcolinear2  24088  brcolinear  24089  colinearperm2  24094  colinearperm4  24095  colinearperm5  24096  brofs2  24107  brifs2  24108  btwnconn1lem3  24119  btwnconn1lem4  24120  btwnconn1lem5  24121  btwnconn1lem8  24124  btwnconn1lem10  24126  btwnconn1lem11  24127  brsegle2  24139  broutsideof3  24156  outsideofeu  24161  lineunray  24177  hfninf  24223  nndivlub  24304  wl-dedlem0a  24329  neleq12d  24331  reubidvag  24333  sbcbidv2  24367  untbi12d  24420  cnvref2  24464  feq123  24466  surjsec2  24519  inttpemp  24538  repcpwti  24560  islatalg  24582  isoriso2  24612  isdir2  24691  grpodlcan  24775  vecval3b  24851  islp3  24913  istopx  24946  prcnt  24950  cnfilca  24955  flfnei2  24976  iintlem1  25009  ismgra  25109  isalg  25120  algi  25126  dualded  25182  ismona  25208  ismonc  25213  iepiclem  25222  isepic  25223  issubcata  25245  issrc  25266  isntr  25272  islimcat  25275  prismorcset  25313  cmppar3  25373  bisig0  25461  iscol2  25492  isibg2  25509  isside1  25564  isside  25565  pdiveql  25567  abhp  25572  abhp1  25573  elicc3  25627  nn0prpwlem  25637  nn0prpw  25638  topfneec  25690  islocfin  25695  neibastop3  25710  neifg  25719  eltail  25722  filnetlem4  25729  euuni2OLD  25747  sdclem2  25851  fdc  25854  lmclim2  25873  0totbnd  25896  sstotbnd  25898  isbnd3b  25908  ismtyval  25923  isismty  25924  ismtyima  25926  heiborlem7  25940  heiborlem10  25943  bfplem1  25945  rrnmet  25952  rrnheibor  25960  ismrer1  25961  isdrngo2  25988  isidlc  26039  ralxpxfr2d  26159  elrfi  26168  elrfirn2  26170  isnacs2  26180  mrefg3  26182  nacsfix  26186  lzunuz  26246  diophin  26251  sbc2rexg  26264  sbc4rexg  26265  sbccomieg  26269  rexrabdioph  26274  4rexfrabdioph  26278  6rexfrabdioph  26279  diophren  26295  fiphp3d  26301  irrapxlem2  26307  elpell1qr2  26356  reglogltb  26375  reglogleb  26376  monotuz  26425  monotoddzz  26427  zindbi  26430  rmyeq0  26439  jm2.19lem2  26482  jm2.19lem3  26483  rmydioph  26506  expdiophlem1  26513  expdioph  26515  pw2f1o2val2  26532  soeq12d  26533  freq12d  26534  weeq12d  26535  fnwe2lem2  26547  islmodfg  26566  islssfg2  26568  dsmmelbas  26604  ellspd  26653  pwfi2f1o  26659  islindf  26681  islbs4  26701  islinds3  26703  islnr3  26718  rngunsnply  26777  f1omvdconj  26788  f1otrspeq  26789  pmtrmvd  26797  idomrootle  26910  caofcan  26939  pm14.122c  27023  pm14.123c  27026  sbaniota  27034  fnchoice  27099  rfcnpre3  27103  rfcnpre4  27104  climinf  27131  stoweidlem7  27155  stoweidlem13  27161  stoweidlem27  27175  stoweidlem34  27182  stoweidlem35  27183  stoweidlem43  27191  stoweidlem59  27207  sbcrel  27352  csbdmg  27353  sbcfun  27358  dfdfat2  27369  fnbrafvb  27393  afvelrnb  27402  dmfcoafv  27413  trsbc  27575  sbcssOLD  27577  bnj984  28251  bnj1417  28338  islshpsm  28437  lrelat  28471  islshpat  28474  islshpcv  28510  ellkr  28546  lkr0f  28551  lkrsc  28554  lshpkrlem1  28567  islshpkrN  28577  lfl1dim  28578  lkrpssN  28620  ldual1dim  28623  ople0  28644  opltn0  28647  op1le  28649  opcon2b  28654  oplecon1b  28658  opltcon1b  28662  opltcon2b  28663  cmtvalN  28668  omllaw4  28703  cmt4N  28709  cmtbr3N  28711  cmtbr4N  28712  omlfh1N  28715  cvrval  28726  pats  28742  leatb  28749  atlle0  28762  atlltn0  28763  cvlatcvr1  28798  cvlatcvr2  28799  ishlat1  28809  glbconxN  28834  hlsupr2  28843  hlateq  28855  hlrelat  28858  hlrelat2  28859  cvrval5  28871  cvrexchlem  28875  atcvr0eq  28882  cvrat4  28899  3dim0  28913  3dim2  28924  2dim  28926  islln3  28966  llnexatN  28977  islpln3  28989  islpln5  28991  islvol3  29032  islvol5  29035  4atlem11  29065  4atlem12  29068  lineset  29194  psubspset  29200  ispsubsp2  29202  elpmapat  29220  pmapglbx  29225  isline3  29232  isline4N  29233  elpaddat  29260  elpadd2at  29262  pmapjoin  29308  dalawlem13  29339  ispsubcl2N  29403  lhpoc  29470  lhpmod2i2  29494  lhpmod6i1  29495  lautset  29538  pautsetN  29554  ltrnatb  29593  ltrnel  29595  ltrncnvel  29598  ltrneq  29605  trlid0b  29634  cdleme0ex2N  29680  cdleme3  29693  cdleme7  29705  cdlemefrs29bpre0  29852  cdlemg2cN  30045  cdlemg2cex  30047  cdlemk34  30366  cdlemkid3N  30389  cdlemkid4  30390  cdlemk39s  30395  cdlemk42  30397  dvhb1dimN  30442  diaord  30504  dia11N  30505  diaglbN  30512  dia1dim2  30519  dvhopellsm  30574  dibelval3  30604  dibopelval3  30605  dibeldmN  30615  dib11N  30617  dib1dim  30622  diblsmopel  30628  diclspsn  30651  dihopelvalbN  30695  dihopelvalcqat  30703  dihopelvalcpre  30705  xihopellsmN  30711  dihopellsm  30712  dihord3  30714  dihord4  30715  dih11  30722  dihglbcpreN  30757  dihmeetlem4preN  30763  dihlspsnat  30790  dihatexv2  30796  dochord2N  30828  dochord3  30829  dochkrshp2  30844  dihjatcclem4  30878  dihjat1lem  30885  dvh2dimatN  30897  lcfl2  30950  lcfl3  30951  lcfl4N  30952  lcfl7N  30958  lcfrvalsnN  30998  lcfrlem9  31007  lcdlss  31076  mapdordlem2  31094  mapd1o  31105  mapdcv  31117  mapdn0  31126  mapdindp  31128  mapdpglem3  31132  mapdpglem26  31155  mapdpglem27  31156  mapdpglem30  31159  mapdindp1  31177  lspindp5  31227  hdmap1ffval  31253  hdmap1fval  31254  hdmapffval  31286  hdmapfval  31287  hdmapeq0  31304  hdmap11  31308  hgmapffval  31345  hgmapfval  31346  hdmapoc  31391  hlhilphllem  31419
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator