MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitrd Structured version   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 4    <-> 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  3bior2fd  1292  dral1  2061  ax11el  2278  eleq12d  2511  neeq12d  2623  neleq12d  2708  raleqbi1dv  2919  rexeqbi1dv  2920  reueqd  2921  rmoeqd  2922  raleqbid  2923  rexeqbid  2924  raleqbidv  2925  rexeqbidv  2926  raleqbidva  2927  rexeqbidva  2928  eueq3  3118  sbc19.21g  3241  sbcrextOLD  3250  sbcrext  3251  sbcabel  3257  sseq12d  3366  psseq12d  3430  sbceq1g  3660  sbcel2gOLD  3662  sbceq2g  3663  sbcco3g  3674  sbccsb2gOLD  3684  raaan  3763  raaanv  3764  sbcss  3766  elimhyp2v  3817  elimhyp4v  3819  keephyp2v  3823  ralsng  3875  rexsng  3876  ssunsn2  3987  2ralunsn  4033  csbunig  4052  disjeq12d  4222  disjprg  4239  breq123d  4257  sbcbr12g  4293  sbcbr1g  4294  sbcbr2g  4295  treq  4339  nalset  4375  copsex4g  4480  frirr  4594  ordtri1  4649  reusv7OLD  4770  reuxfr2d  4781  reuxfrd  4783  elpwun  4791  ordpwsuc  4830  ordunisuc2  4859  tfindsg  4875  dfom2  4882  findsg  4907  csbxpg  4940  posn  4981  frsn  4983  csbrng  5149  elrelimasn  5263  eliniseg  5268  brcodir  5288  fneq12d  5573  feq12d  5617  feq123d  5618  f1osng  5751  csbfv12  5796  csbfv12gOLD  5797  dmfco  5833  eqfnfv2  5864  fndmdifeq0  5872  fneqeql2  5875  funimass3  5882  funconstss  5884  unpreima  5892  ralrnmpt  5914  dffo3  5920  fmptco  5937  fressnfv  5956  fnsuppeq0  5989  fnunirn  6035  f1elima  6045  cocan1  6060  cocan2  6061  fliftf  6073  soisores  6083  isomin  6093  isoini  6094  f1oiso  6107  f1oweALT  6110  mpt2eq123dva  6171  ovid  6226  ov  6229  ovg  6248  caovord2d  6292  ofrfval2  6359  offveqb  6362  reldm  6434  mpt2xopoveq  6506  mpt2xopovel  6507  isprmpt2  6513  tpostpos  6535  f1ofveu  6620  oe0m1  6801  oaord1  6830  omord  6847  omlimcl  6857  oewordi  6870  oeeui  6881  nnaordr  6899  nnaordex  6917  ereq1  6948  brdifun  6968  erth2  6986  qliftfun  7025  brecop  7033  elmapg  7067  elpmg  7068  boxcutc  7141  dom2lem  7183  xpcomco  7234  pw2f1olem  7248  nndomo  7336  unfilem2  7408  domunfican  7415  indexfi  7450  elfi2  7455  supisolem  7511  hartogslem1  7547  brwdom2  7577  canthwdom  7583  infeq5i  7627  cantnfs  7657  cantnfrescl  7668  cantnfp1lem3  7672  cantnflem1b  7678  cantnflem1  7681  cnfcom3lem  7696  r1pwOLD  7808  rankxplim  7841  iscard2  7901  infxpenc2  7941  fseqenlem1  7943  fseqdom  7945  alephnbtwn  7990  alephinit  8014  iunfictbso  8033  dfac2  8049  dfac12lem2  8062  dfac12lem3  8063  kmlem2  8069  ackbij2lem2  8158  fin23lem23  8244  fin1a2lem2  8319  fin1a2lem4  8321  fin1a2lem9  8326  dcomex  8365  axdclem  8437  brdom7disj  8447  brdom6disj  8448  iundom2g  8453  axpownd  8514  fpwwe2cbv  8543  fpwwe2lem2  8545  fpwwe2lem3  8546  fpwwe2lem9  8551  fpwwe2  8556  pwfseqlem1  8571  eltskm  8756  ltapi  8818  ltmpi  8819  nlt1pi  8821  indpi  8822  nqereu  8844  ordpipq  8857  ltsonq  8884  ltanq  8886  ltrnq  8894  archnq  8895  elnpi  8903  genpass  8924  addclprlem1  8931  mulclprlem  8934  1idpr  8944  prlem934  8948  prlem936  8962  reclem4pr  8965  addgt0sr  9017  sqgt0sr  9019  ltresr  9053  leloe  9199  eqlelt  9200  negeu  9334  subadd2  9347  subcan2  9364  ltadd1  9533  leadd2  9535  ltsubadd  9536  lesubadd  9538  ltaddsub2  9541  leaddsub2  9543  ltaddpos  9556  lesub2  9561  ltnegcon1  9567  ltnegcon2  9568  lenegcon1  9570  lenegcon2  9571  addge01  9576  addge02  9577  suble0  9580  lesub0  9582  eqord2  9596  mulcan2d  9694  diveq0  9726  diveq1  9746  ltmul2  9899  lemul2  9901  ltmulgt11  9908  ltmulgt12  9909  gt0div  9914  ge0div  9915  ltmuldiv  9918  ledivmul2OLD  9926  ltdiv2  9933  ltrec1  9935  lerec2  9936  ledivdiv  9937  ltdiv23  9939  lediv23  9940  creur  10032  creui  10033  ofsubeq0  10035  nn1suc  10059  nnrecl  10257  nn0sub  10308  znnsub  10360  btwnnz  10384  gtndiv  10385  uzindOLD  10402  eluz2  10532  uzwo  10577  uzwoOLD  10578  indstr2  10592  negn0  10600  rpneg  10679  xrleloe  10775  xltadd2  10874  xsubge0  10878  xlesubadd  10880  xmulasslem  10902  xlemul2  10908  xltmul2  10910  supxrre2  10948  elixx3g  10967  ioo0  10979  iccid  10999  ico0  11000  ioc0  11001  icc0  11002  elioc2  11011  elico2  11012  elicc2  11013  elfz2  11088  fzen  11110  fzsubel  11126  fzpr  11139  fzrevral2  11170  fzrevral3  11171  fzshftral  11172  fzosplitsni  11234  btwnzge0  11268  mod0  11293  negmod0  11294  nn0ennn  11356  expeq0  11448  sq11  11492  sq01  11539  hashen  11669  hashnncl  11683  hashsdom  11693  seqcoll2  11751  ccatopth2  11815  cnpart  12083  sqrlem7  12092  sqrneglem  12110  sqabs  12150  abslt  12156  absle  12157  absdiflt  12159  absdifle  12160  lenegsq  12162  rexanuz2  12191  limsupgle  12309  limsuple  12310  clim  12326  rlim  12327  clim0c  12339  rlim0  12340  rlim0lt  12341  ello12  12348  ello1mpt  12353  elo12  12359  lo1o12  12365  elo1mpt  12366  elo1mpt2  12367  o1lo1  12369  isercolllem2  12497  isercoll2  12500  zsum  12550  fsum2dlem  12592  fsumcom2  12596  binomlem  12646  efieq  12802  sin01bnd  12824  cos01bnd  12825  dvdsval2  12893  dvdsaddr  12927  fzocongeq  12941  odd2np1  12946  divalglem4  12954  divalglem5  12955  divalgb  12962  bits0  12978  bitsp1e  12982  bitsp1o  12983  bitscmp  12988  bitsinv1lem  12991  sadval  13006  sadcaddlem  13007  smuval  13031  smuval2  13032  dvdssq  13098  nn0seqcvgd  13099  algcvgblem  13106  isprm2  13125  qredeq  13144  prmdvdsexp  13152  prmdvdsexpb  13153  prmexpb  13155  prmfac1  13156  qnumgt0  13180  hashdvds  13202  fermltl  13211  pcpremul  13255  pc2dvds  13290  pcz  13292  prmpwdvds  13310  prmreclem5  13326  4sqlem16  13366  vdwapun  13380  vdwmc  13384  vdwlem6  13392  ramval  13414  prdsbasmpt  13730  prdsleval  13737  prdsbasmpt2  13742  imasleval  13804  xpsle  13844  mrcidb2  13881  ismri  13894  mrieqvd  13901  acsfiel  13917  acsfn2  13926  catpropd  13973  ismon2  13998  isepi2  14005  isinv  14023  isssc  14058  subsubc  14088  funcres2b  14132  funcpropd  14135  isfull  14145  isfth  14149  fullpropd  14155  isnat2  14183  fucsect  14207  fuciso  14210  elsetchom  14274  setcsect  14282  setciso  14284  isprs  14425  isdrs  14429  posi  14445  pltval3  14462  istos  14502  islat  14514  latleeqj1  14530  latleeqj2  14531  latleeqm1  14546  latleeqm2  14547  ipodrsima  14629  isacs5  14636  acsficl2d  14640  isdlat  14657  mhmpropd  14782  issubm2  14787  gsumvalx  14812  gsumpropd  14814  grpsubrcan  14908  grplactcnv  14925  issubg  14982  eqgval  15027  conjnmzb  15078  isga  15106  odmulg  15230  odf1o1  15244  odngen  15249  gexdvds  15256  pgpfi2  15278  isslw  15280  slwpss  15284  pgpssslw  15286  subgslw  15288  sylow2alem2  15290  fislw  15297  sylow3lem2  15300  lsmelvalm  15323  lsmdisj3a  15359  pj1eq  15370  iscmn  15457  eqgabl  15492  torsubg  15507  gsumval3  15552  dprdf11  15619  dprd2da  15638  dmdprdpr  15645  ablfac1eulem  15668  pgpfac1lem2  15671  pgpfac1lem3a  15672  pgpfac1lem3  15673  rngpropd  15733  dvdsrval  15788  dvdsr02  15799  unitpropd  15840  drngmuleq0  15896  drngpropd  15900  issubrg  15906  islmod  15992  lsmelpr  16201  lspsnne1  16227  fidomndrnglem  16404  coe1mul2lem2  16699  coe1tm  16703  prmirredlem  16811  prmirred  16813  domnchr  16851  znleval  16873  znchr  16881  znunithash  16883  iscss2  16951  ishil2  16984  istopg  17006  eltg  17060  eltg2  17061  tgss2  17090  bastop1  17096  bastop2  17097  iscld  17129  iscld4  17167  elcls2  17176  elcls3  17185  isclo  17189  mretopd  17194  isnei  17205  neiint  17206  neindisj2  17225  islp2  17247  islp3  17248  maxlp  17249  cldlp  17252  neitr  17282  iscn  17337  iscnp  17339  iscnp3  17346  tgcn  17354  subbascn  17356  ssidcn  17357  lmbr2  17361  lmbrf  17362  cnnei  17384  cnrest2  17388  hausnei2  17455  cmpsub  17501  tgcmp  17502  cmpfi  17509  consuba  17521  connsub  17522  dis2ndc  17561  subislly  17582  elkgen  17606  kgencn  17626  kgencn2  17627  eltx  17638  ptpjpre1  17641  ptcnplem  17691  hausdiag  17715  xkoptsub  17724  xkoco2cn  17728  imasnopn  17760  imasncld  17761  imasncls  17762  elqtop  17767  qtopcld  17783  kqcldsat  17803  kqt0lem  17806  isr0  17807  regr1lem2  17810  ordthmeolem  17871  ptuncnv  17877  trfbas  17914  elfg  17941  trfil3  17958  trufil  17980  filufint  17990  uffix2  17994  elfm2  18018  elfm3  18020  flimtopon  18040  flimopn  18045  fbflim  18046  fbflim2  18047  flffbas  18065  flftg  18066  cnflf  18072  txflf  18076  isfcls  18079  fclstopon  18082  fclsbas  18091  fclsrest  18094  fcfnei  18105  cnfcf  18112  ptcmplem2  18122  tgphaus  18184  tgpt0  18186  divstgphaus  18190  tsmsgsum  18206  tsmsres  18211  tsmsxplem1  18220  isust  18271  elutop  18301  utopsnneiplem  18315  utopsnnei  18317  isusp  18329  isucn  18346  isucn2  18347  ucncn  18353  ispsmet  18373  ismet  18391  isxmet  18392  metn0  18428  xmetres2  18429  elbl3ps  18459  elbl3  18460  xblpnfps  18463  xblpnf  18464  elmopn2  18513  metss  18576  stdbdxmet  18583  metcnp3  18608  metcnp  18609  metcnp2  18610  metcn  18611  txmetcnp  18615  txmetcn  18616  cfilucfil2OLD  18641  cfilucfil2  18642  blval2  18643  metuelOLD  18645  metuel  18646  metuel2  18647  metucnOLD  18656  metucn  18657  dscopn  18659  isngp3  18683  nmeq0  18702  ngppropd  18716  isnghm3  18797  isnmhm2  18824  bl2ioo  18861  metdsge  18917  metnrmlem1a  18926  addcnlem  18932  elcncf  18957  elcncf2  18958  evth  19022  elpi1  19108  nmhmcn  19166  cphipeq0  19204  ipcau2  19229  lmmbr  19249  lmmbr2  19250  iscfil2  19257  fmcfil  19263  iscau2  19268  iscau3  19269  iscau4  19270  iscauf  19271  caucfil  19274  metcld2  19297  cfilucfil4OLD  19311  cfilucfil4  19312  bcthlem1  19315  lssbn  19342  cmetcusp1OLD  19343  cmetcusp1  19344  srabn  19352  ishl2  19362  minveclem7  19374  ivth2  19390  ovolfioo  19402  ovolficc  19403  ovolshftlem1  19443  ovolicc2lem1  19451  icombl  19496  ioombl  19497  volsup2  19535  ismbf  19558  ismbfcn  19559  ismbfcn2  19567  mbfmax  19577  mbfimaopnlem  19583  mbfaddlem  19588  mbfsup  19592  mbfinf  19593  mbflimsup  19594  i1faddlem  19621  i1fres  19633  itg1ge0a  19639  itg1climres  19642  mbfi1fseqlem4  19646  itg2leub  19662  itg2const  19668  itg2split  19677  itg2cnlem2  19690  iblcnlem1  19715  iblrelem  19718  itgss3  19742  ellimc  19798  ellimc2  19802  ellimc3  19804  limcmpt  19808  limcmpt2  19809  limcres  19811  cnplimc  19812  limcun  19820  dvreslem  19834  dvcnp  19843  dvcnvlem  19898  dveflem  19901  cmvth  19913  mdegleb  20025  mdegldg  20027  degltp1le  20034  mdegle0  20038  deg1ldg  20053  coe1mul3  20060  ply1remlem  20123  fta1glem2  20127  ply1termlem  20160  coemulc  20211  coecj  20234  plymul0or  20236  ofmulrt  20237  quotval  20247  plydivlem4  20251  plyremlem  20259  ulmcau2  20350  reeff1o  20401  sincosq2sgn  20445  sinq12gt0  20453  coseq1  20468  logltb  20532  cosarg0d  20542  argrege0  20544  tanarg  20552  affineequiv  20705  dcubic1lem  20721  dcubic  20724  atandm2  20755  rlimcnp  20842  rlimcnp2  20843  xrlimcnp  20845  fsumharmonic  20888  wilthlem1  20889  ftalem7  20899  basellem3  20903  isppw2  20936  issqf  20957  sqf11  20960  mumullem2  21001  sqff1o  21003  muinv  21016  ppiublem1  21024  vmasum  21038  chpchtsum  21041  chpub  21042  dchrelbas2  21059  dchrelbas3  21060  dchrelbas4  21065  dchrinv  21083  efexple  21103  bposlem1  21106  bposlem6  21111  bposlem7  21112  lgsdilem  21144  lgsdir2lem4  21148  lgsdir2  21150  lgsne0  21155  lgsabs1  21156  lgsquad3  21183  2sqlem7  21192  2sqlem8a  21193  chtppilim  21207  dchrvmaeq0  21236  dirith  21261  ostth3  21370  isumgra  21388  wrdumgra  21389  isusgra0  21414  nbgrael  21476  nbgraeledg  21480  nb3graprlem1  21498  nb3grapr2  21501  cusgra2v  21509  cusgra3vnbpr  21512  cusgrafilem3  21528  cusgrauvtxb  21543  iswlk  21565  iswlkon  21569  trls  21574  istrl  21575  istrl2  21576  istrlon  21579  ispth  21606  isspth  21607  0spth  21609  ispthon  21614  isspthon  21621  isspthonpth  21622  1pthon  21629  wlkdvspthlem  21645  0crct  21651  0cycl  21652  fargshiftfva  21664  iseupa  21725  eupatrl  21728  eupath2lem2  21738  eupath2lem3  21739  isgrpo  21822  isablo  21909  ismgm  21946  opidon2  21950  ismndo1  21970  elghomlem2  21988  iscom2  22038  rngosn3  22052  rngosn4  22053  vci  22065  isvclem  22094  vcoprnelem  22095  nvsubadd  22174  nvelbl  22223  nvelbl2  22224  nmoubi  22311  nmobndi  22314  nmoo0  22330  isph  22361  minvecolem4b  22418  minvecolem4  22420  minvecolem5  22421  minvecolem7  22423  h2hcau  22520  h2hlm  22521  hvaddeq0  22609  hial2eq2  22647  norm-i  22669  hhssnv  22802  shsel  22854  shsel3  22855  pjhtheu2  22956  chssoc  23036  chsscon1  23041  chpsscon1  23044  chpsscon2  23045  chlejb2  23053  elspansn2  23107  fh1  23158  fh2  23159  cm2j  23160  eigposi  23377  nmopub  23449  unopf1o  23457  nmfnleub  23466  elnlfn  23469  adjvalval  23478  lnopcnre  23580  riesz4i  23604  leop2  23665  leop3  23666  leoppos  23667  hst1h  23768  mdbr2  23837  mdbr3  23838  mdbr4  23839  dmdbr2  23844  dmdbr3  23846  dmdbr4  23847  mddmd2  23850  cvdmd  23878  atcvatlem  23926  atdmd  23939  sumdmdii  23956  dmdbr5ati  23963  cdj3lem1  23975  addltmulALT  23987  reuxfr3d  24012  reuxfr4d  24013  iuneq12daf  24043  csbcnvg  24072  abfmpeld  24101  abfmpel  24102  fmptdF  24104  fmptcof2  24111  disjdsct  24125  xeqlelt  24174  tltnle  24225  gsumpropd2lem  24255  isofld  24270  isinftm  24286  isarchi  24287  metidv  24322  pstmxmet  24327  lmxrge0  24372  zrhker  24396  esumlub  24487  issiga  24529  dya2ub  24655  itgeq12dv  24676  orvcgteel  24760  ballotlemfc0  24785  ballotlemfcc  24786  ballotlemrv1  24813  ballotlemrv2  24814  ballotlem1ri  24827  derangval  24888  derangenlem  24892  subfacp1lem2a  24901  subfacp1lem5  24905  erdszelem8  24919  iccllyscon  24972  cvmsval  24988  untelirr  25192  untsucf  25194  untangtr  25198  mulcan2g  25225  mulle0b  25227  mulsuble0b  25228  zprod  25298  fprodcom2  25343  dfpo2  25413  dfon2lem3  25447  dfon2lem4  25448  dfon2lem7  25451  elpredim  25486  predep  25502  preduz  25510  brbtwn  25873  brcgr  25874  eqeelen  25878  brbtwn2  25879  colinearalglem1  25880  colinearalglem2  25881  colinearalglem3  25882  colinearalg  25884  axcgrid  25890  ax5seglem4  25906  ax5seglem5  25907  axbtwnid  25913  axcontlem5  25942  axcontlem7  25944  cgrcomlr  25967  ifscgr  26013  cgr3permute2  26018  cgr3permute4  26019  cgr3permute5  26020  brcolinear2  26027  brcolinear  26028  colinearperm2  26033  colinearperm4  26034  colinearperm5  26035  brofs2  26046  brifs2  26047  btwnconn1lem3  26058  btwnconn1lem4  26059  btwnconn1lem5  26060  btwnconn1lem8  26063  btwnconn1lem10  26065  btwnconn1lem11  26066  brsegle2  26078  broutsideof3  26095  outsideofeu  26100  lineunray  26116  hfninf  26162  nndivlub  26243  wl-dedlem0a  26267  ltflcei  26275  itg2addnclem2  26299  itg2addnclem3  26300  itg2gt0cn  26302  itgaddnclem2  26306  iblabsnclem  26310  ftc1anclem1  26322  ftc1anclem5  26326  ftc1anclem7  26328  dvreasin  26332  areacirclem1  26334  areacirclem4  26337  areacirclem5  26338  areacirc  26339  elicc3  26362  nn0prpwlem  26367  nn0prpw  26368  topfneec  26413  islocfin  26418  neibastop3  26433  neifg  26442  eltail  26445  filnetlem4  26452  sdclem2  26488  fdc  26491  lmclim2  26506  0totbnd  26524  sstotbnd  26526  isbnd3b  26536  ismtyval  26551  isismty  26552  ismtyima  26554  heiborlem7  26568  heiborlem10  26571  bfplem1  26573  rrnmet  26580  rrnheibor  26588  ismrer1  26589  isdrngo2  26616  isidlc  26667  iineq12f  26792  ralxpxfr2d  26853  elrfi  26860  elrfirn2  26862  isnacs2  26872  mrefg3  26874  nacsfix  26878  lzunuz  26938  diophin  26943  sbc2rexg  26956  sbc4rexg  26957  sbccomieg  26961  rexrabdioph  26966  4rexfrabdioph  26970  6rexfrabdioph  26971  diophren  26986  fiphp3d  26992  irrapxlem2  26998  elpell1qr2  27047  reglogltb  27066  reglogleb  27067  monotuz  27116  monotoddzz  27118  zindbi  27121  rmyeq0  27130  jm2.19lem2  27173  jm2.19lem3  27174  rmydioph  27197  expdiophlem1  27204  expdioph  27206  pw2f1o2val2  27223  soeq12d  27224  freq12d  27225  weeq12d  27226  fnwe2lem2  27238  islmodfg  27256  islssfg2  27258  dsmmelbas  27294  ellspd  27343  pwfi2f1o  27349  islindf  27371  islbs4  27391  islinds3  27393  islnr3  27408  rngunsnply  27467  f1omvdconj  27478  f1otrspeq  27479  pmtrmvd  27487  idomrootle  27600  caofcan  27629  pm14.122c  27713  pm14.123c  27716  sbaniota  27724  fnchoice  27788  rfcnpre3  27792  rfcnpre4  27793  climinf  27820  stoweidlem7  27844  stoweidlem27  27864  stoweidlem35  27872  sbcrel  28069  csbdmg  28070  sbcfun  28075  dfdfat2  28083  fnbrafvb  28106  afvelrnb  28115  dmfcoafv  28127  otthg  28177  sbcfn  28188  sbcf  28189  f12dfv  28196  f13dfv  28197  leaddle0  28214  2ffzeq  28242  ubmelm1fzo  28248  2ffzoeq  28261  csbwrdg  28298  wrdeq0  28302  swdeq  28328  modprm1div  28356  modprminveq  28358  cshwsiun  28418  wlkcomp  28437  usgra2pth  28447  usgra2pth0  28448  el2wlkonot  28499  el2spthonot  28500  el2spthonot0  28501  el2wlkonotot1  28504  el2wlksotot  28512  usg2wlkonot  28513  usg2wotspth  28514  2spontn0vne  28517  usg2spthonot0  28519  usg2spthonot1  28520  2spot2iun2spont  28521  nbhashuvtx1  28529  usgrauvtxvdbi  28532  isrusgra  28540  frgra3v  28564  frgrancvvdeqlem3  28593  frgrawopreglem2  28606  usg2spot2nb  28626  usgreg2spot  28628  trsbc  28797  sbcssOLD  28799  csbfv12gALT  29108  bnj984  29497  bnj1417  29584  islshpsm  29952  lrelat  29986  islshpat  29989  islshpcv  30025  ellkr  30061  lkr0f  30066  lkrsc  30069  lshpkrlem1  30082  islshpkrN  30092  lfl1dim  30093  lkrpssN  30135  ldual1dim  30138  ople0  30159  opltn0  30162  op1le  30164  opcon2b  30169  oplecon1b  30173  opltcon1b  30177  opltcon2b  30178  cmtvalN  30183  omllaw4  30218  cmt4N  30224  cmtbr3N  30226  cmtbr4N  30227  omlfh1N  30230  cvrval  30241  pats  30257  leatb  30264  atlle0  30277  atlltn0  30278  cvlatcvr1  30313  cvlatcvr2  30314  ishlat1  30324  glbconxN  30349  hlsupr2  30358  hlateq  30370  hlrelat  30373  hlrelat2  30374  cvrval5  30386  cvrexchlem  30390  atcvr0eq  30397  cvrat4  30414  3dim0  30428  3dim2  30439  2dim  30441  islln3  30481  llnexatN  30492  islpln3  30504  islpln5  30506  islvol3  30547  islvol5  30550  4atlem11  30580  4atlem12  30583  lineset  30709  psubspset  30715  ispsubsp2  30717  elpmapat  30735  pmapglbx  30740  isline3  30747  isline4N  30748  elpaddat  30775  elpadd2at  30777  pmapjoin  30823  dalawlem13  30854  ispsubcl2N  30918  lhpoc  30985  lhpmod2i2  31009  lhpmod6i1  31010  lautset  31053  pautsetN  31069  ltrnatb  31108  ltrnel  31110  ltrncnvel  31113  ltrneq  31120  trlid0b  31149  cdleme0ex2N  31195  cdleme3  31208  cdleme7  31220  cdlemefrs29bpre0  31367  cdlemg2cN  31560  cdlemg2cex  31562  cdlemk34  31881  cdlemkid3N  31904  cdlemkid4  31905  cdlemk39s  31910  cdlemk42  31912  dvhb1dimN  31957  diaord  32019  dia11N  32020  diaglbN  32027  dia1dim2  32034  dvhopellsm  32089  dibelval3  32119  dibopelval3  32120  dibeldmN  32130  dib11N  32132  dib1dim  32137  diblsmopel  32143  diclspsn  32166  dihopelvalbN  32210  dihopelvalcqat  32218  dihopelvalcpre  32220  xihopellsmN  32226  dihopellsm  32227  dihord3  32229  dihord4  32230  dih11  32237  dihglbcpreN  32272  dihmeetlem4preN  32278  dihlspsnat  32305  dihatexv2  32311  dochord2N  32343  dochord3  32344  dochkrshp2  32359  dihjatcclem4  32393  dihjat1lem  32400  dvh2dimatN  32412  lcfl2  32465  lcfl3  32466  lcfl4N  32467  lcfl7N  32473  lcfrvalsnN  32513  lcfrlem9  32522  lcdlss  32591  mapdordlem2  32609  mapd1o  32620  mapdcv  32632  mapdn0  32641  mapdindp  32643  mapdpglem3  32647  mapdpglem26  32670  mapdpglem27  32671  mapdpglem30  32674  mapdindp1  32692  lspindp5  32742  hdmap1ffval  32768  hdmap1fval  32769  hdmapffval  32801  hdmapfval  32802  hdmapeq0  32819  hdmap11  32823  hgmapffval  32860  hgmapfval  32861  hdmapoc  32906  hlhilphllem  32934
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 179
  Copyright terms: Public domain W3C validator