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

Theorem bitrd 244
Description: Deduction form of bitri 240. (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 236 . . 3  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
3 bitrd.2 . . . 4  |-  ( ph  ->  ( ch  <->  th )
)
43pm5.74i 236 . . 3  |-  ( (
ph  ->  ch )  <->  ( ph  ->  th ) )
52, 4bitri 240 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  th ) )
65pm5.74ri 237 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  bitr2d  245  bitr3d  246  bitr4d  247  syl5bb  248  syl6bb  252  3bitrd  270  3bitr2d  272  3bitr3d  274  3bitr4d  276  imbi12d  311  bibi12d  312  sylan9bb  680  orbi12d  690  anbi12d  691  dedlem0a  918  ax11el  2133  eleq12d  2351  neeq12d  2461  raleqbi1dv  2744  rexeqbi1dv  2745  reueqd  2746  rmoeqd  2747  raleqbidv  2748  rexeqbidv  2749  raleqbidva  2750  rexeqbidva  2751  eueq3  2940  sbc19.21g  3055  sbcrext  3064  sbcabel  3068  sbcel1g  3100  sbceq1g  3101  sbcel2g  3102  sbceq2g  3103  sbccsb2g  3110  sbcco3g  3136  sseq12d  3207  psseq12d  3270  raaan  3561  raaanv  3562  sbcss  3564  elimhyp2v  3614  elimhyp4v  3616  keephyp2v  3620  ralsng  3672  rexsng  3673  ssunsn2  3773  2ralunsn  3816  csbunig  3835  disjeq12d  4002  disjprg  4019  breq123d  4037  sbcbr12g  4073  sbcbr1g  4074  sbcbr2g  4075  treq  4119  nalset  4151  copsex4g  4255  frirr  4370  ordtri1  4425  reusv7OLD  4546  reuxfr2d  4557  reuxfrd  4559  elpwun  4567  ordpwsuc  4606  ordunisuc2  4635  tfindsg  4651  dfom2  4658  findsg  4683  csbxpg  4716  posn  4758  frsn  4760  csbrng  4923  elrelimasn  5037  eliniseg  5042  brcodir  5062  fneq12d  5337  feq12d  5381  feq123d  5382  f1osng  5514  f1oprswap  5515  csbfv12g  5535  csbfv12gALT  5536  dmfco  5593  eqfnfv2  5623  fndmdifeq0  5631  fneqeql2  5634  funimass3  5641  funconstss  5643  unpreima  5651  ralrnmpt  5669  dffo3  5675  fmptco  5691  fressnfv  5707  fnsuppeq0  5733  fnunirn  5778  f1elima  5787  cocan1  5801  cocan2  5802  fliftf  5814  soisores  5824  isomin  5834  isoini  5835  f1oiso  5848  f1oweALT  5851  mpt2eq123dva  5909  ovid  5964  ov  5967  ovg  5986  caovord2d  6029  ofrfval2  6096  offveqb  6099  reldm  6171  tpostpos  6254  f1ofveu  6339  oe0m1  6520  oaord1  6549  omord  6566  omlimcl  6576  oewordi  6589  oeeui  6600  nnaordr  6618  nnaordex  6636  ereq1  6667  brdifun  6687  erth2  6705  qliftfun  6743  brecop  6751  elmapg  6785  elpmg  6786  boxcutc  6859  dom2lem  6901  xpcomco  6952  pw2f1olem  6966  nndomo  7054  unfilem2  7122  domunfican  7129  indexfi  7163  elfi2  7168  supisolem  7221  hartogslem1  7257  brwdom2  7287  canthwdom  7293  infeq5i  7337  cantnfs  7367  cantnfrescl  7378  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1  7391  cnfcom3lem  7406  r1pwOLD  7518  rankxplim  7549  iscard2  7609  infxpenc2  7649  fseqenlem1  7651  fseqdom  7653  alephnbtwn  7698  alephinit  7722  iunfictbso  7741  dfac2  7757  dfac12lem2  7770  dfac12lem3  7771  kmlem2  7777  ackbij2lem2  7866  fin23lem23  7952  fin1a2lem2  8027  fin1a2lem4  8029  fin1a2lem9  8034  dcomex  8073  axdclem  8146  brdom7disj  8156  brdom6disj  8157  iundom2g  8162  axpownd  8223  fpwwe2cbv  8252  fpwwe2lem2  8254  fpwwe2lem3  8255  fpwwe2lem9  8260  fpwwe2  8265  pwfseqlem1  8280  eltskm  8465  ltapi  8527  ltmpi  8528  nlt1pi  8530  indpi  8531  nqereu  8553  ordpipq  8566  ltsonq  8593  ltanq  8595  ltrnq  8603  archnq  8604  elnpi  8612  genpass  8633  addclprlem1  8640  mulclprlem  8643  1idpr  8653  prlem934  8657  prlem936  8671  reclem4pr  8674  addgt0sr  8726  sqgt0sr  8728  ltresr  8762  leloe  8908  eqlelt  8909  negeu  9042  subadd2  9055  subcan2  9072  ltadd1  9241  leadd2  9243  ltsubadd  9244  lesubadd  9246  ltaddsub2  9249  leaddsub2  9251  ltaddpos  9264  lesub2  9269  ltnegcon1  9275  ltnegcon2  9276  lenegcon1  9278  lenegcon2  9279  addge01  9284  addge02  9285  suble0  9288  lesub0  9290  eqord2  9304  mulcan2d  9402  diveq0  9434  diveq1  9454  ltmul2  9607  lemul2  9609  ltmulgt11  9616  ltmulgt12  9617  gt0div  9622  ge0div  9623  ltmuldiv  9626  ledivmul2OLD  9634  ltdiv2  9641  ltrec1  9643  lerec2  9644  ledivdiv  9645  ltdiv23  9647  lediv23  9648  creur  9740  creui  9741  ofsubeq0  9743  nn1suc  9767  nnrecl  9963  nn0sub  10014  znnsub  10064  btwnnz  10088  gtndiv  10089  uzindOLD  10106  eluz2  10236  uzwo  10281  uzwoOLD  10282  indstr2  10296  negn0  10304  rpneg  10383  xrleloe  10478  xltadd2  10577  xsubge0  10581  xlesubadd  10583  xmulasslem  10605  xlemul2  10611  xltmul2  10613  supxrre2  10650  elixx3g  10669  ioo0  10681  iccid  10701  ico0  10702  ioc0  10703  icc0  10704  elioc2  10713  elico2  10714  elicc2  10715  elfz2  10789  fzen  10811  fzsubel  10827  fzpr  10840  fzrevral2  10867  fzrevral3  10868  fzshftral  10869  fzosplitsni  10921  btwnzge0  10953  mod0  10978  negmod0  10979  nn0ennn  11041  expeq0  11132  sq11  11176  sq01  11223  hashen  11346  hashnncl  11354  hashsdom  11363  seqcoll2  11402  ccatopth2  11463  cnpart  11725  sqrlem7  11734  sqrneglem  11752  sqabs  11792  abslt  11798  absle  11799  absdiflt  11801  absdifle  11802  lenegsq  11804  rexanuz2  11833  limsupgle  11951  limsuple  11952  clim  11968  rlim  11969  clim0c  11981  rlim0  11982  rlim0lt  11983  ello12  11990  ello1mpt  11995  elo12  12001  lo1o12  12007  elo1mpt  12008  elo1mpt2  12009  o1lo1  12011  isercolllem2  12139  isercoll2  12142  zsum  12191  fsum2dlem  12233  fsumcom2  12237  binomlem  12287  efieq  12443  sin01bnd  12465  cos01bnd  12466  dvdsval2  12534  dvdsaddr  12568  fzocongeq  12582  odd2np1  12587  divalglem4  12595  divalglem5  12596  divalgb  12603  bits0  12619  bitsp1e  12623  bitsp1o  12624  bitscmp  12629  bitsinv1lem  12632  sadval  12647  sadcaddlem  12648  smuval  12672  smuval2  12673  dvdssq  12739  nn0seqcvgd  12740  algcvgblem  12747  isprm2  12766  qredeq  12785  prmdvdsexp  12793  prmdvdsexpb  12794  prmexpb  12796  prmfac1  12797  qnumgt0  12821  hashdvds  12843  fermltl  12852  pcpremul  12896  pc2dvds  12931  pcz  12933  prmpwdvds  12951  prmreclem5  12967  4sqlem16  13007  vdwapun  13021  vdwmc  13025  vdwlem6  13033  ramval  13055  prdsbasmpt  13369  prdsleval  13376  prdsbasmpt2  13381  imasleval  13443  xpsle  13483  mrcidb2  13520  ismri  13533  mrieqvd  13540  acsfiel  13556  acsfn2  13565  catpropd  13612  cidpropd  13613  ismon2  13637  isepi2  13644  isinv  13662  isssc  13697  subsubc  13727  funcres2b  13771  funcpropd  13774  isfull  13784  isfth  13788  fullpropd  13794  isnat2  13822  fucsect  13846  fuciso  13849  elsetchom  13913  setcsect  13921  setciso  13923  evlfcl  13996  isprs  14064  isdrs  14068  posi  14084  pltval3  14101  istos  14141  islat  14153  latleeqj1  14169  latleeqj2  14170  latleeqm1  14185  latleeqm2  14186  ipodrsima  14268  isacs5  14275  acsficl2d  14279  isdlat  14296  ismgmid  14387  mhmpropd  14421  issubm2  14426  gsumvalx  14451  gsumpropd  14453  grpsubrcan  14547  grplactcnv  14564  issubg  14621  eqgval  14666  conjnmzb  14717  isga  14745  odmulg  14869  odf1o1  14883  odngen  14888  gexdvds  14895  pgpfi2  14917  isslw  14919  slwpss  14923  pgpssslw  14925  subgslw  14927  sylow2alem2  14929  fislw  14936  sylow3lem2  14939  lsmelvalm  14962  lsmdisj3a  14998  pj1eq  15009  iscmn  15096  eqgabl  15131  torsubg  15146  gsumval3  15191  dprdf11  15258  dprd2da  15277  dmdprdpr  15284  ablfac1eulem  15307  pgpfac1lem2  15310  pgpfac1lem3a  15311  pgpfac1lem3  15312  rngpropd  15372  dvdsrval  15427  dvdsr02  15438  unitpropd  15479  drngmuleq0  15535  drngpropd  15539  issubrg  15545  islmod  15631  lsmelpr  15844  lspsnne1  15870  fidomndrnglem  16047  coe1mul2lem2  16345  coe1tm  16349  prmirredlem  16446  prmirred  16448  domnchr  16486  znleval  16508  znchr  16516  znunithash  16518  iscss2  16586  ishil2  16619  istopg  16641  eltg  16695  eltg2  16696  tgss2  16725  bastop1  16731  bastop2  16732  iscld  16764  iscld4  16802  elcls2  16811  elcls3  16820  isclo  16824  mretopd  16829  isnei  16840  neiint  16841  neindisj2  16860  islp2  16877  maxlp  16878  cldlp  16881  iscn  16965  iscnp  16967  iscnp3  16974  tgcn  16982  subbascn  16984  ssidcn  16985  lmbr2  16989  lmbrf  16990  cnrest2  17014  hausnei2  17081  cmpsub  17127  tgcmp  17128  cmpfi  17135  consuba  17146  connsub  17147  dis2ndc  17186  subislly  17207  elkgen  17231  kgencn  17251  kgencn2  17252  eltx  17263  ptpjpre1  17266  ptcnplem  17315  hausdiag  17339  xkoptsub  17348  xkoco2cn  17352  elqtop  17388  qtopcld  17404  kqcldsat  17424  kqt0lem  17427  isr0  17428  regr1lem2  17431  ordthmeolem  17492  ptuncnv  17498  trfbas  17539  elfg  17566  trfil3  17583  trufil  17605  filufint  17615  uffix2  17619  elfm2  17643  elfm3  17645  flimtopon  17665  flimopn  17670  fbflim  17671  fbflim2  17672  flffbas  17690  flftg  17691  cnflf  17697  txflf  17701  isfcls  17704  fclstopon  17707  fclsbas  17716  fclsrest  17719  fcfnei  17730  cnfcf  17737  ptcmplem2  17747  tgphaus  17799  tgpt0  17801  divstgphaus  17805  tsmsgsum  17821  tsmsres  17826  tsmsxplem1  17835  ismet  17888  isxmet  17889  metn0  17924  xmetres2  17925  elbl3  17951  xblpnf  17953  elmopn2  17991  metss  18054  stdbdxmet  18061  metcnp3  18086  metcnp  18087  metcnp2  18088  metcn  18089  txmetcnp  18093  txmetcn  18094  dscopn  18096  isngp3  18120  nmeq0  18139  ngppropd  18153  isnghm3  18234  isnmhm2  18261  bl2ioo  18298  metdsge  18353  metnrmlem1a  18362  addcnlem  18368  elcncf  18393  elcncf2  18394  evth  18457  elpi1  18543  nmhmcn  18601  cphipeq0  18639  ipcau2  18664  lmmbr  18684  lmmbr2  18685  iscfil2  18692  fmcfil  18698  iscau  18702  iscau2  18703  iscau3  18704  iscau4  18705  iscauf  18706  caucfil  18709  metcld2  18732  bcthlem1  18746  lssbn  18773  srabn  18777  ishl2  18787  minveclem7  18799  ivth2  18815  ovolfioo  18827  ovolficc  18828  ovolshftlem1  18868  ovolicc2lem1  18876  icombl  18921  ioombl  18922  volsup2  18960  ismbf  18985  ismbfcn  18986  ismbfcn2  18994  mbfmax  19004  mbfimaopnlem  19010  mbfaddlem  19015  mbfsup  19019  mbfinf  19020  mbflimsup  19021  i1faddlem  19048  i1fres  19060  itg1ge0a  19066  itg1climres  19069  mbfi1fseqlem4  19073  itg2leub  19089  itg2const  19095  itg2split  19104  itg2cnlem2  19117  iblcnlem1  19142  iblrelem  19145  itgss3  19169  ellimc  19223  ellimc2  19227  ellimc3  19229  limcmpt  19233  limcmpt2  19234  limcres  19236  cnplimc  19237  limcun  19245  dvreslem  19259  dvcnp  19268  dvcnvlem  19323  dveflem  19326  cmvth  19338  mdegleb  19450  mdegldg  19452  degltp1le  19459  mdegle0  19463  deg1ldg  19478  coe1mul3  19485  ply1remlem  19548  fta1glem2  19552  ply1termlem  19585  coemulc  19636  coecj  19659  plymul0or  19661  ofmulrt  19662  quotval  19672  plydivlem4  19676  plyremlem  19684  ulmcau2  19773  reeff1o  19823  sincosq2sgn  19867  sinq12gt0  19875  coseq1  19890  logltb  19953  cosarg0d  19963  argrege0  19965  tanarg  19970  affineequiv  20123  dcubic1lem  20139  dcubic  20142  atandm2  20173  rlimcnp  20260  rlimcnp2  20261  xrlimcnp  20263  fsumharmonic  20305  wilthlem1  20306  ftalem7  20316  basellem3  20320  isppw2  20353  issqf  20374  sqf11  20377  mumullem2  20418  sqff1o  20420  muinv  20433  ppiublem1  20441  vmasum  20455  chpchtsum  20458  chpub  20459  dchrelbas2  20476  dchrelbas3  20477  dchrelbas4  20482  dchrinv  20500  efexple  20520  bposlem1  20523  bposlem6  20528  bposlem7  20529  lgsdilem  20561  lgsdir2lem4  20565  lgsdir2  20567  lgsne0  20572  lgsabs1  20573  lgsquad3  20600  2sqlem7  20609  2sqlem8a  20610  chtppilim  20624  dchrvmaeq0  20653  dirith  20678  ostth3  20787  isgrpo  20863  isablo  20950  ismgm  20987  opidon2  20991  ismndo1  21011  elghomlem2  21029  isrngo  21045  iscom2  21079  rngosn3  21093  rngosn4  21094  vci  21104  isvclem  21133  vcoprnelem  21134  nvsubadd  21213  nvelbl  21262  nvelbl2  21263  nmoubi  21350  nmobndi  21353  nmoo0  21369  isph  21400  minvecolem4b  21457  minvecolem4  21459  minvecolem5  21460  minvecolem7  21462  h2hcau  21559  h2hlm  21560  hvaddeq0  21648  hial2eq2  21686  norm-i  21708  hhssnv  21841  shsel  21893  shsel3  21894  pjhtheu2  21995  chssoc  22075  chsscon1  22080  chpsscon1  22083  chpsscon2  22084  chlejb2  22092  elspansn2  22146  fh1  22197  fh2  22198  cm2j  22199  eigposi  22416  nmopub  22488  unopf1o  22496  nmfnleub  22505  elnlfn  22508  adjvalval  22517  lnopcnre  22619  riesz4i  22643  leop2  22704  leop3  22705  leoppos  22706  hst1h  22807  mdbr2  22876  mdbr3  22877  mdbr4  22878  dmdbr2  22883  dmdbr3  22885  dmdbr4  22886  mddmd2  22889  cvdmd  22917  atcvatlem  22965  atdmd  22978  sumdmdii  22995  dmdbr5ati  23002  cdj3lem1  23014  addltmulALT  23026  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemrv  23078  ballotlemrv1  23079  ballotlemrv2  23080  ballotlem1ri  23093  derangval  23109  derangenlem  23113  subfacp1lem2a  23122  subfacp1lem5  23126  erdszelem8  23140  iccllyscon  23192  cvmsval  23208  isumgra  23278  wrdumgra  23279  iseupa  23292  eupath2lem2  23313  eupath2lem3  23314  untelirr  23465  untsucf  23467  untangtr  23471  mulcan2g  23496  mulle0b  23498  mulsuble0b  23499  dfpo2  23523  dfon2lem3  23552  dfon2lem4  23553  dfon2lem7  23556  elpredim  23587  predep  23603  preduz  23611  brbtwn  23938  brcgr  23939  eqeelen  23943  brbtwn2  23944  colinearalglem1  23945  colinearalglem2  23946  colinearalglem3  23947  colinearalg  23949  axcgrid  23955  ax5seglem4  23971  ax5seglem5  23972  axbtwnid  23978  axcontlem5  24007  axcontlem7  24009  cgrcomlr  24032  ifscgr  24078  cgr3permute2  24083  cgr3permute4  24084  cgr3permute5  24085  brcolinear2  24092  brcolinear  24093  colinearperm2  24098  colinearperm4  24099  colinearperm5  24100  brofs2  24111  brifs2  24112  btwnconn1lem3  24123  btwnconn1lem4  24124  btwnconn1lem5  24125  btwnconn1lem8  24128  btwnconn1lem10  24130  btwnconn1lem11  24131  brsegle2  24143  broutsideof3  24160  outsideofeu  24165  lineunray  24181  hfninf  24227  nndivlub  24308  wl-dedlem0a  24333  dvreasin  24334  areacirclem2  24337  areacirclem5  24341  areacirclem6  24342  areacirc  24343  neleq12d  24345  reubidvag  24347  sbcbidv2  24381  untbi12d  24434  cnvref2  24478  feq123  24480  surjsec2  24532  inttpemp  24551  repcpwti  24573  islatalg  24595  isoriso2  24625  isdir2  24704  grpodlcan  24788  vecval3b  24864  islp3  24926  istopx  24959  prcnt  24963  cnfilca  24968  flfnei2  24989  iintlem1  25022  ismgra  25122  isalg  25133  algi  25139  dualded  25195  ismona  25221  ismonc  25226  iepiclem  25235  isepic  25236  issubcata  25258  issrc  25279  isntr  25285  islimcat  25288  prismorcset  25326  cmppar3  25386  bisig0  25474  iscol2  25505  isibg2  25522  isside1  25577  isside  25578  pdiveql  25580  abhp  25585  abhp1  25586  elicc3  25640  nn0prpwlem  25650  nn0prpw  25651  topfneec  25703  islocfin  25708  neibastop3  25723  neifg  25732  eltail  25735  filnetlem4  25742  euuni2OLD  25760  sdclem2  25864  fdc  25867  lmclim2  25886  0totbnd  25909  sstotbnd  25911  isbnd3b  25921  ismtyval  25936  isismty  25937  ismtyima  25939  heiborlem7  25953  heiborlem10  25956  bfplem1  25958  rrnmet  25965  rrnheibor  25973  ismrer1  25974  isdrngo2  26001  isidlc  26052  ralxpxfr2d  26172  elrfi  26181  elrfirn2  26183  isnacs2  26193  mrefg3  26195  nacsfix  26199  lzunuz  26259  diophin  26264  sbc2rexg  26277  sbc4rexg  26278  sbccomieg  26282  rexrabdioph  26287  4rexfrabdioph  26291  6rexfrabdioph  26292  diophren  26308  fiphp3d  26314  irrapxlem2  26320  elpell1qr2  26369  reglogltb  26388  reglogleb  26389  monotuz  26438  monotoddzz  26440  zindbi  26443  rmyeq0  26452  jm2.19lem2  26495  jm2.19lem3  26496  rmydioph  26519  expdiophlem1  26526  expdioph  26528  pw2f1o2val2  26545  soeq12d  26546  freq12d  26547  weeq12d  26548  fnwe2lem2  26560  islmodfg  26579  islssfg2  26581  dsmmelbas  26617  ellspd  26666  pwfi2f1o  26672  islindf  26694  islbs4  26714  islinds3  26716  islnr3  26731  rngunsnply  26790  f1omvdconj  26801  f1otrspeq  26802  pmtrmvd  26810  idomrootle  26923  caofcan  26952  pm14.122c  27036  pm14.123c  27039  sbaniota  27047  fnchoice  27112  rfcnpre3  27116  rfcnpre4  27117  climinf  27144  stoweidlem7  27168  stoweidlem13  27174  stoweidlem27  27188  stoweidlem34  27195  stoweidlem35  27196  stoweidlem43  27204  stoweidlem59  27220  sbcrel  27391  csbdmg  27392  sbcfun  27397  dfdfat2  27406  fnbrafvb  27428  afvelrnb  27437  dmfcoafv  27448  isusgra0  27505  frgra3v  27542  trsbc  27677  sbcssOLD  27679  bnj984  28357  bnj1417  28444  islshpsm  28543  lrelat  28577  islshpat  28580  islshpcv  28616  ellkr  28652  lkr0f  28657  lkrsc  28660  lshpkrlem1  28673  islshpkrN  28683  lfl1dim  28684  lkrpssN  28726  ldual1dim  28729  ople0  28750  opltn0  28753  op1le  28755  opcon2b  28760  oplecon1b  28764  opltcon1b  28768  opltcon2b  28769  cmtvalN  28774  omllaw4  28809  cmt4N  28815  cmtbr3N  28817  cmtbr4N  28818  omlfh1N  28821  cvrval  28832  pats  28848  leatb  28855  atlle0  28868  atlltn0  28869  cvlatcvr1  28904  cvlatcvr2  28905  ishlat1  28915  glbconxN  28940  hlsupr2  28949  hlateq  28961  hlrelat  28964  hlrelat2  28965  cvrval5  28977  cvrexchlem  28981  atcvr0eq  28988  cvrat4  29005  3dim0  29019  3dim2  29030  2dim  29032  islln3  29072  llnexatN  29083  islpln3  29095  islpln5  29097  islvol3  29138  islvol5  29141  4atlem11  29171  4atlem12  29174  lineset  29300  psubspset  29306  ispsubsp2  29308  elpmapat  29326  pmapglbx  29331  isline3  29338  isline4N  29339  elpaddat  29366  elpadd2at  29368  pmapjoin  29414  dalawlem13  29445  ispsubcl2N  29509  lhpoc  29576  lhpmod2i2  29600  lhpmod6i1  29601  lautset  29644  pautsetN  29660  ltrnatb  29699  ltrnel  29701  ltrncnvel  29704  ltrneq  29711  trlid0b  29740  cdleme0ex2N  29786  cdleme3  29799  cdleme7  29811  cdlemefrs29bpre0  29958  cdlemg2cN  30151  cdlemg2cex  30153  cdlemk34  30472  cdlemkid3N  30495  cdlemkid4  30496  cdlemk39s  30501  cdlemk42  30503  dvhb1dimN  30548  diaord  30610  dia11N  30611  diaglbN  30618  dia1dim2  30625  dvhopellsm  30680  dibelval3  30710  dibopelval3  30711  dibeldmN  30721  dib11N  30723  dib1dim  30728  diblsmopel  30734  diclspsn  30757  dihopelvalbN  30801  dihopelvalcqat  30809  dihopelvalcpre  30811  xihopellsmN  30817  dihopellsm  30818  dihord3  30820  dihord4  30821  dih11  30828  dihglbcpreN  30863  dihmeetlem4preN  30869  dihlspsnat  30896  dihatexv2  30902  dochord2N  30934  dochord3  30935  dochkrshp2  30950  dihjatcclem4  30984  dihjat1lem  30991  dvh2dimatN  31003  lcfl2  31056  lcfl3  31057  lcfl4N  31058  lcfl7N  31064  lcfrvalsnN  31104  lcfrlem9  31113  lcdlss  31182  mapdordlem2  31200  mapd1o  31211  mapdcv  31223  mapdn0  31232  mapdindp  31234  mapdpglem3  31238  mapdpglem26  31261  mapdpglem27  31262  mapdpglem30  31265  mapdindp1  31283  lspindp5  31333  hdmap1ffval  31359  hdmap1fval  31360  hdmapffval  31392  hdmapfval  31393  hdmapeq0  31410  hdmap11  31414  hgmapffval  31451  hgmapfval  31452  hdmapoc  31497  hlhilphllem  31525
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
  Copyright terms: Public domain W3C validator