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  683  orbi12d  693  anbi12d  694  dedlem0a  923  ax11el  2110  eleq12d  2326  neeq12d  2436  raleqbi1dv  2719  rexeqbi1dv  2720  reueqd  2721  rmoeqd  2722  raleqbidv  2723  rexeqbidv  2724  raleqbidva  2725  rexeqbidva  2726  eueq3  2915  sbc19.21g  3030  sbcrext  3039  sbcabel  3043  sbcel1g  3075  sbceq1g  3076  sbcel2g  3077  sbceq2g  3078  sbccsb2g  3085  sbcco3g  3111  sseq12d  3182  psseq12d  3245  raaan  3536  raaanv  3537  elimhyp2v  3588  elimhyp4v  3590  keephyp2v  3594  ralsng  3646  rexsng  3647  ssunsn2  3747  2ralunsn  3790  csbunig  3809  disjeq12d  3976  disjprg  3993  breq123d  4011  sbcbr12g  4047  sbcbr1g  4048  sbcbr2g  4049  treq  4093  nalset  4125  copsex4g  4227  frirr  4342  ordtri1  4397  reusv7OLD  4518  reuxfr2d  4529  reuxfrd  4531  elpwun  4539  ordpwsuc  4578  ordunisuc2  4607  tfindsg  4623  dfom2  4630  findsg  4655  csbxpg  4704  posn  4746  frsn  4748  csbrng  4911  elrelimasn  5025  eliniseg  5030  brcodir  5050  fneq12d  5275  feq12d  5319  feq123d  5320  f1osng  5452  f1oprswap  5453  fv2  5454  csbfv12g  5468  csbfv12gALT  5469  dmfco  5527  eqfnfv2  5557  fndmdifeq0  5565  fneqeql2  5568  funimass3  5575  funconstss  5577  unpreima  5585  ralrnmpt  5603  dffo3  5609  fmptco  5625  fressnfv  5641  fnsuppeq0  5667  fnunirn  5712  f1elima  5721  cocan1  5735  cocan2  5736  fliftf  5748  soisores  5758  isomin  5768  isoini  5769  f1oiso  5782  f1oweALT  5785  mpt2eq123dva  5843  ovid  5898  ov  5901  ovg  5920  caovord2d  5963  ofrfval2  6030  offveqb  6033  reldm  6105  tpostpos  6188  f1ofveu  6307  oe0m1  6488  oaord1  6517  omord  6534  omlimcl  6544  oewordi  6557  oeeui  6568  nnaordr  6586  nnaordex  6604  ereq1  6635  brdifun  6655  erth2  6673  qliftfun  6711  brecop  6719  elmapg  6753  elpmg  6754  boxcutc  6827  dom2lem  6869  xpcomco  6920  pw2f1olem  6934  nndomo  7022  unfilem2  7090  domunfican  7097  indexfi  7131  elfi2  7136  supisolem  7189  hartogslem1  7225  brwdom2  7255  canthwdom  7261  infeq5i  7305  cantnfs  7335  cantnfrescl  7346  cantnfp1lem3  7350  cantnflem1b  7356  cantnflem1  7359  cnfcom3lem  7374  r1pwOLD  7486  rankxplim  7517  iscard2  7577  infxpenc2  7617  fseqenlem1  7619  fseqdom  7621  alephnbtwn  7666  alephinit  7690  iunfictbso  7709  dfac2  7725  dfac12lem2  7738  dfac12lem3  7739  kmlem2  7745  ackbij2lem2  7834  fin23lem23  7920  fin1a2lem2  7995  fin1a2lem4  7997  fin1a2lem9  8002  dcomex  8041  axdclem  8114  brdom7disj  8124  brdom6disj  8125  iundom2g  8130  axpownd  8191  fpwwe2cbv  8220  fpwwe2lem2  8222  fpwwe2lem3  8223  fpwwe2lem9  8228  fpwwe2  8233  pwfseqlem1  8248  eltskm  8433  ltapi  8495  ltmpi  8496  nlt1pi  8498  indpi  8499  nqereu  8521  ordpipq  8534  ltsonq  8561  ltanq  8563  ltrnq  8571  archnq  8572  elnpi  8580  genpass  8601  addclprlem1  8608  mulclprlem  8611  1idpr  8621  prlem934  8625  prlem936  8639  reclem4pr  8642  addgt0sr  8694  sqgt0sr  8696  ltresr  8730  leloe  8876  eqlelt  8877  negeu  9010  subadd2  9023  subcan2  9040  ltadd1  9209  leadd2  9211  ltsubadd  9212  lesubadd  9214  ltaddsub2  9217  leaddsub2  9219  ltaddpos  9232  lesub2  9237  ltnegcon1  9243  ltnegcon2  9244  lenegcon1  9246  lenegcon2  9247  addge01  9252  addge02  9253  suble0  9256  lesub0  9258  eqord2  9272  mulcan2d  9370  diveq0  9402  diveq1  9422  ltmul2  9575  lemul2  9577  ltmulgt11  9584  ltmulgt12  9585  gt0div  9590  ge0div  9591  ltmuldiv  9594  ledivmul2OLD  9602  ltdiv2  9609  ltrec1  9611  lerec2  9612  ledivdiv  9613  ltdiv23  9615  lediv23  9616  creur  9708  creui  9709  ofsubeq0  9711  nn1suc  9735  nnrecl  9930  nn0sub  9981  znnsub  10031  btwnnz  10055  gtndiv  10056  uzindOLD  10073  eluz2  10203  uzwo  10248  uzwoOLD  10249  indstr2  10263  negn0  10271  rpneg  10350  xrleloe  10445  xltadd2  10543  xsubge0  10547  xlesubadd  10549  xmulasslem  10571  xlemul2  10577  xltmul2  10579  supxrre2  10616  elixx3g  10635  ioo0  10647  iccid  10667  ico0  10668  ioc0  10669  icc0  10670  elioc2  10679  elico2  10680  elicc2  10681  elfz2  10755  fzen  10777  fzsubel  10793  fzpr  10806  fzrevral2  10833  fzrevral3  10834  fzshftral  10835  fzosplitsni  10887  btwnzge0  10919  mod0  10944  negmod0  10945  nn0ennn  11007  expeq0  11098  sq11  11142  sq01  11189  hashen  11312  hashnncl  11320  hashsdom  11329  seqcoll2  11367  ccatopth2  11428  cnpart  11690  sqrlem7  11699  sqrneglem  11717  sqabs  11757  abslt  11763  absle  11764  absdiflt  11766  absdifle  11767  lenegsq  11769  rexanuz2  11798  limsupgle  11916  limsuple  11917  clim  11933  rlim  11934  clim0c  11946  rlim0  11947  rlim0lt  11948  ello12  11955  ello1mpt  11960  elo12  11966  lo1o12  11972  elo1mpt  11973  elo1mpt2  11974  o1lo1  11976  isercolllem2  12104  isercoll2  12107  zsum  12156  fsum2dlem  12198  fsumcom2  12202  binomlem  12252  efieq  12405  sin01bnd  12427  cos01bnd  12428  divides2  12496  dvdsaddr  12530  fzocongeq  12544  odd2np1  12549  divalglem4  12557  divalglem5  12558  divalgb  12565  bits0  12581  bitsp1e  12585  bitsp1o  12586  bitscmp  12591  bitsinv1lem  12594  sadval  12609  sadcaddlem  12610  smuval  12634  smuval2  12635  dvdssq  12701  nn0seqcvgd  12702  algcvgblem  12709  isprm2  12728  qredeq  12747  prmdvdsexp  12755  prmdvdsexpb  12756  prmexpb  12758  prmfac1  12759  qnumgt0  12783  hashdvds  12805  fermltl  12814  pcpremul  12858  pc2dvds  12893  pcz  12895  prmpwdvds  12913  prmreclem5  12929  4sqlem16  12969  vdwapun  12983  vdwmc  12987  vdwlem6  12995  ramval  13017  prdsbasmpt  13331  prdsleval  13338  prdsbasmpt2  13343  imasleval  13405  xpsle  13445  mrcidb2  13482  ismri  13495  mrieqvd  13502  acsfiel  13518  acsfn2  13527  catpropd  13574  cidpropd  13575  ismon2  13599  isepi2  13606  isinv  13624  isssc  13659  subsubc  13689  funcres2b  13733  funcpropd  13736  isfull  13746  isfth  13750  fullpropd  13756  isnat2  13784  fucsect  13808  fuciso  13811  elsetchom  13875  setcsect  13883  setciso  13885  evlfcl  13958  isprs  14026  isdrs  14030  posi  14046  pltval3  14063  istos  14103  islat  14115  latleeqj1  14131  latleeqj2  14132  latleeqm1  14147  latleeqm2  14148  ipodrsima  14230  isacs5  14237  acsficl2d  14241  isdlat  14258  ismgmid  14349  mhmpropd  14383  issubm2  14388  gsumvalx  14413  gsumpropd  14415  grpsubrcan  14509  grplactcnv  14526  issubg  14583  eqgval  14628  conjnmzb  14679  isga  14707  odmulg  14831  odf1o1  14845  odngen  14850  gexdvds  14857  pgpfi2  14879  isslw  14881  slwpss  14885  pgpssslw  14887  subgslw  14889  sylow2alem2  14891  fislw  14898  sylow3lem2  14901  lsmelvalm  14924  lsmdisj3a  14960  pj1eq  14971  iscmn  15058  eqgabl  15093  torsubg  15108  gsumval3  15153  dprdf11  15220  dprd2da  15239  dmdprdpr  15246  ablfac1eulem  15269  pgpfac1lem2  15272  pgpfac1lem3a  15273  pgpfac1lem3  15274  rngpropd  15334  dvdsrval  15389  dvdsr02  15400  unitpropd  15441  drngmuleq0  15497  drngpropd  15501  issubrg  15507  islmod  15593  lsmelpr  15806  lspsnne1  15832  fidomndrnglem  16009  coe1mul2lem2  16307  coe1tm  16311  prmirredlem  16408  prmirred  16410  domnchr  16448  znleval  16470  znchr  16478  znunithash  16480  iscss2  16548  ishil2  16581  istopg  16603  eltg  16657  eltg2  16658  tgss2  16687  bastop1  16693  bastop2  16694  iscld  16726  iscld4  16764  elcls2  16773  elcls3  16782  isclo  16786  mretopd  16791  isnei  16802  neiint  16803  neindisj2  16822  islp2  16839  maxlp  16840  cldlp  16843  iscn  16927  iscnp  16929  iscnp3  16936  tgcn  16944  subbascn  16946  ssidcn  16947  lmbr2  16951  lmbrf  16952  cnrest2  16976  hausnei2  17043  cmpsub  17089  tgcmp  17090  cmpfi  17097  consuba  17108  connsub  17109  dis2ndc  17148  subislly  17169  elkgen  17193  kgencn  17213  kgencn2  17214  eltx  17225  ptpjpre1  17228  ptcnplem  17277  hausdiag  17301  xkoptsub  17310  xkoco2cn  17314  elqtop  17350  qtopcld  17366  kqcldsat  17386  kqt0lem  17389  isr0  17390  regr1lem2  17393  ordthmeolem  17454  ptuncnv  17460  trfbas  17501  elfg  17528  trfil3  17545  trufil  17567  filufint  17577  uffix2  17581  elfm2  17605  elfm3  17607  flimtopon  17627  flimopn  17632  fbflim  17633  fbflim2  17634  flffbas  17652  flftg  17653  cnflf  17659  txflf  17663  isfcls  17666  fclstopon  17669  fclsbas  17678  fclsrest  17681  fcfnei  17692  cnfcf  17699  ptcmplem2  17709  tgphaus  17761  tgpt0  17763  divstgphaus  17767  tsmsgsum  17783  tsmsres  17788  tsmsxplem1  17797  ismet  17850  isxmet  17851  metn0  17886  xmetres2  17887  elbl3  17913  xblpnf  17915  elmopn2  17953  metss  18016  stdbdxmet  18023  metcnp3  18048  metcnp  18049  metcnp2  18050  metcn  18051  txmetcnp  18055  txmetcn  18056  dscopn  18058  isngp3  18082  nmeq0  18101  ngppropd  18115  isnghm3  18196  isnmhm2  18223  bl2ioo  18260  metdsge  18315  metnrmlem1a  18324  addcnlem  18330  elcncf  18355  elcncf2  18356  evth  18419  elpi1  18505  nmhmcn  18563  cphipeq0  18601  ipcau2  18626  lmmbr  18646  lmmbr2  18647  iscfil2  18654  fmcfil  18660  iscau  18664  iscau2  18665  iscau3  18666  iscau4  18667  iscauf  18668  caucfil  18671  metcld2  18694  bcthlem1  18708  lssbn  18735  srabn  18739  ishl2  18749  minveclem7  18761  ivth2  18777  ovolfioo  18789  ovolficc  18790  ovolshftlem1  18830  ovolicc2lem1  18838  icombl  18883  ioombl  18884  volsup2  18922  ismbf  18947  ismbfcn  18948  ismbfcn2  18956  mbfmax  18966  mbfimaopnlem  18972  mbfaddlem  18977  mbfsup  18981  mbfinf  18982  mbflimsup  18983  i1faddlem  19010  i1fres  19022  itg1ge0a  19028  itg1climres  19031  mbfi1fseqlem4  19035  itg2leub  19051  itg2const  19057  itg2split  19066  itg2cnlem2  19079  iblcnlem1  19104  iblrelem  19107  itgss3  19131  ellimc  19185  ellimc2  19189  ellimc3  19191  limcmpt  19195  limcmpt2  19196  limcres  19198  cnplimc  19199  limcun  19207  dvreslem  19221  dvcnp  19230  dvcnvlem  19285  dveflem  19288  cmvth  19300  mdegleb  19412  mdegldg  19414  degltp1le  19421  mdegle0  19425  deg1ldg  19440  coe1mul3  19447  ply1remlem  19510  fta1glem2  19514  ply1termlem  19547  coemulc  19598  coecj  19621  plymul0or  19623  ofmulrt  19624  quotval  19634  plydivlem4  19638  plyremlem  19646  ulmcau2  19735  reeff1o  19785  sincosq2sgn  19829  sinq12gt0  19837  coseq1  19852  logltb  19915  cosarg0d  19925  argrege0  19927  tanarg  19932  affineequiv  20085  dcubic1lem  20101  dcubic  20104  atandm2  20135  rlimcnp  20222  rlimcnp2  20223  xrlimcnp  20225  fsumharmonic  20267  wilthlem1  20268  ftalem7  20278  basellem3  20282  isppw2  20315  issqf  20336  sqf11  20339  mumullem2  20380  sqff1o  20382  muinv  20395  ppiublem1  20403  vmasum  20417  chpchtsum  20420  chpub  20421  dchrelbas2  20438  dchrelbas3  20439  dchrelbas4  20444  dchrinv  20462  efexple  20482  bposlem1  20485  bposlem6  20490  bposlem7  20491  lgsdilem  20523  lgsdir2lem4  20527  lgsdir2  20529  lgsne0  20534  lgsabs1  20535  lgsquad3  20562  2sqlem7  20571  2sqlem8a  20572  chtppilim  20586  dchrvmaeq0  20615  dirith  20640  ostth3  20749  isgrpo  20823  isablo  20910  ismgm  20947  opidon2  20951  ismndo1  20971  elghomlem2  20989  isrngo  21005  iscom2  21039  rngosn3  21053  rngosn4  21054  vci  21064  isvclem  21093  vcoprnelem  21094  nvsubadd  21173  nvelbl  21222  nvelbl2  21223  nmoubi  21310  nmobndi  21313  nmoo0  21329  isph  21360  minvecolem4b  21417  minvecolem4  21419  minvecolem5  21420  minvecolem7  21422  h2hcau  21519  h2hlm  21520  hvaddeq0  21608  hial2eq2  21646  norm-i  21668  hhssnv  21801  shsel  21853  shsel3  21854  pjhtheu2  21955  chssoc  22035  chsscon1  22040  chpsscon1  22043  chpsscon2  22044  chlejb2  22052  elspansn2  22106  fh1  22157  fh2  22158  cm2j  22159  eigposi  22376  nmopub  22448  unopf1o  22456  nmfnleub  22465  elnlfn  22468  adjvalval  22477  lnopcnre  22579  riesz4i  22603  leop2  22664  leop3  22665  leoppos  22666  hst1h  22767  mdbr2  22836  mdbr3  22837  mdbr4  22838  dmdbr2  22843  dmdbr3  22845  dmdbr4  22846  mddmd2  22849  cvdmd  22877  atcvatlem  22925  atdmd  22938  sumdmdii  22955  dmdbr5ati  22962  cdj3lem1  22974  addltmulALT  22986  ballotlemfc0  23012  ballotlemfcc  23013  ballotlemrv  23039  ballotlemrv1  23040  ballotlemrv2  23041  ballotlem1ri  23054  derangval  23070  derangenlem  23074  subfacp1lem2a  23083  subfacp1lem5  23087  erdszelem8  23101  iccllyscon  23153  cvmsval  23169  isumgra  23239  wrdumgra  23240  iseupa  23253  eupath2lem2  23274  eupath2lem3  23275  untelirr  23426  untsucf  23428  untangtr  23432  mulcan2g  23456  mulle0b  23458  mulsuble0b  23459  dfpo2  23483  dfon2lem3  23510  dfon2lem4  23511  dfon2lem7  23514  elpredim  23545  predep  23561  preduz  23569  brbtwn  23902  brcgr  23903  eqeelen  23907  brbtwn2  23908  colinearalglem1  23909  colinearalglem2  23910  colinearalglem3  23911  colinearalg  23913  axcgrid  23919  ax5seglem4  23935  ax5seglem5  23936  axbtwnid  23942  axcontlem5  23971  axcontlem7  23973  cgrcomlr  23996  ifscgr  24042  cgr3permute2  24047  cgr3permute4  24048  cgr3permute5  24049  brcolinear2  24056  brcolinear  24057  colinearperm2  24062  colinearperm4  24063  colinearperm5  24064  brofs2  24075  brifs2  24076  btwnconn1lem3  24087  btwnconn1lem4  24088  btwnconn1lem5  24089  btwnconn1lem8  24092  btwnconn1lem10  24094  btwnconn1lem11  24095  brsegle2  24107  broutsideof3  24124  outsideofeu  24129  lineunray  24145  hfninf  24191  nndivlub  24272  wl-dedlem0a  24297  neleq12d  24299  reubidvag  24301  sbcbidv2  24335  untbi12d  24388  cnvref2  24432  feq123  24434  surjsec2  24487  inttpemp  24506  repcpwti  24528  islatalg  24550  isoriso2  24580  isdir2  24659  grpodlcan  24743  vecval3b  24819  islp3  24881  istopx  24914  prcnt  24918  cnfilca  24923  flfnei2  24944  iintlem1  24977  ismgra  25077  isalg  25088  algi  25094  dualded  25150  ismona  25176  ismonc  25181  iepiclem  25190  isepic  25191  issubcata  25213  issrc  25234  isntr  25240  islimcat  25243  prismorcset  25281  cmppar3  25341  bisig0  25429  iscol2  25460  isibg2  25477  isside1  25532  isside  25533  pdiveql  25535  abhp  25540  abhp1  25541  elicc3  25595  nn0prpwlem  25605  nn0prpw  25606  topfneec  25658  islocfin  25663  neibastop3  25678  neifg  25687  eltail  25690  filnetlem4  25697  euuni2OLD  25715  sdclem2  25819  fdc  25822  lmclim2  25841  0totbnd  25864  sstotbnd  25866  isbnd3b  25876  ismtyval  25891  isismty  25892  ismtyima  25894  heiborlem7  25908  heiborlem10  25911  bfplem1  25913  rrnmet  25920  rrnheibor  25928  ismrer1  25929  isdrngo2  25956  isidlc  26007  ralxpxfr2d  26127  elrfi  26136  elrfirn2  26138  isnacs2  26148  mrefg3  26150  nacsfix  26154  lzunuz  26214  diophin  26219  sbc2rexg  26232  sbc4rexg  26233  sbccomieg  26237  rexrabdioph  26242  4rexfrabdioph  26246  6rexfrabdioph  26247  diophren  26263  fiphp3d  26269  irrapxlem2  26275  elpell1qr2  26324  reglogltb  26343  reglogleb  26344  monotuz  26393  monotoddzz  26395  zindbi  26398  rmyeq0  26407  jm2.19lem2  26450  jm2.19lem3  26451  rmydioph  26474  expdiophlem1  26481  expdioph  26483  pw2f1o2val2  26500  soeq12d  26501  freq12d  26502  weeq12d  26503  fnwe2lem2  26515  islmodfg  26534  islssfg2  26536  dsmmelbas  26572  ellspd  26621  pwfi2f1o  26627  islindf  26649  islbs4  26669  islinds3  26671  islnr3  26686  rngunsnply  26745  f1omvdconj  26756  f1otrspeq  26757  pmtrmvd  26765  idomrootle  26878  caofcan  26907  pm14.122c  26992  pm14.123c  26995  sbaniota  27003  fnchoice  27068  rfcnpre3  27072  rfcnpre4  27073  stoweidlem7  27091  stoweidlem13  27097  stoweidlem27  27111  stoweidlem34  27118  stoweidlem35  27119  stoweidlem43  27127  stoweidlem59  27143  trsbc  27357  sbcss  27359  bnj984  28033  bnj1417  28120  islshpsm  28337  lrelat  28371  islshpat  28374  islshpcv  28410  ellkr  28446  lkr0f  28451  lkrsc  28454  lshpkrlem1  28467  islshpkrN  28477  lfl1dim  28478  lkrpssN  28520  ldual1dim  28523  ople0  28544  opltn0  28547  op1le  28549  opcon2b  28554  oplecon1b  28558  opltcon1b  28562  opltcon2b  28563  cmtvalN  28568  omllaw4  28603  cmt4N  28609  cmtbr3N  28611  cmtbr4N  28612  omlfh1N  28615  cvrval  28626  pats  28642  leatb  28649  atlle0  28662  atlltn0  28663  cvlatcvr1  28698  cvlatcvr2  28699  ishlat1  28709  glbconxN  28734  hlsupr2  28743  hlateq  28755  hlrelat  28758  hlrelat2  28759  cvrval5  28771  cvrexchlem  28775  atcvr0eq  28782  cvrat4  28799  3dim0  28813  3dim2  28824  2dim  28826  islln3  28866  llnexatN  28877  islpln3  28889  islpln5  28891  islvol3  28932  islvol5  28935  4atlem11  28965  4atlem12  28968  lineset  29094  psubspset  29100  ispsubsp2  29102  elpmapat  29120  pmapglbx  29125  isline3  29132  isline4N  29133  elpaddat  29160  elpadd2at  29162  pmapjoin  29208  dalawlem13  29239  ispsubcl2N  29303  lhpoc  29370  lhpmod2i2  29394  lhpmod6i1  29395  lautset  29438  pautsetN  29454  ltrnatb  29493  ltrnel  29495  ltrncnvel  29498  ltrneq  29505  trlid0b  29534  cdleme0ex2N  29580  cdleme3  29593  cdleme7  29605  cdlemefrs29bpre0  29752  cdlemg2cN  29945  cdlemg2cex  29947  cdlemk34  30266  cdlemkid3N  30289  cdlemkid4  30290  cdlemk39s  30295  cdlemk42  30297  dvhb1dimN  30342  diaord  30404  dia11N  30405  diaglbN  30412  dia1dim2  30419  dvhopellsm  30474  dibelval3  30504  dibopelval3  30505  dibeldmN  30515  dib11N  30517  dib1dim  30522  diblsmopel  30528  diclspsn  30551  dihopelvalbN  30595  dihopelvalcqat  30603  dihopelvalcpre  30605  xihopellsmN  30611  dihopellsm  30612  dihord3  30614  dihord4  30615  dih11  30622  dihglbcpreN  30657  dihmeetlem4preN  30663  dihlspsnat  30690  dihatexv2  30696  dochord2N  30728  dochord3  30729  dochkrshp2  30744  dihjatcclem4  30778  dihjat1lem  30785  dvh2dimatN  30797  lcfl2  30850  lcfl3  30851  lcfl4N  30852  lcfl7N  30858  lcfrvalsnN  30898  lcfrlem9  30907  lcdlss  30976  mapdordlem2  30994  mapd1o  31005  mapdcv  31017  mapdn0  31026  mapdindp  31028  mapdpglem3  31032  mapdpglem26  31055  mapdpglem27  31056  mapdpglem30  31059  mapdindp1  31077  lspindp5  31127  hdmap1ffval  31153  hdmap1fval  31154  hdmapffval  31186  hdmapfval  31187  hdmapeq0  31204  hdmap11  31208  hgmapffval  31245  hgmapfval  31246  hdmapoc  31291  hlhilphllem  31319
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