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

Theorem bitrd 245
Description: Deduction form of bitri 241. (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 237 . . 3  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
3 bitrd.2 . . . 4  |-  ( ph  ->  ( ch  <->  th )
)
43pm5.74i 237 . . 3  |-  ( (
ph  ->  ch )  <->  ( ph  ->  th ) )
52, 4bitri 241 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  th ) )
65pm5.74ri 238 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  bitr2d  246  bitr3d  247  bitr4d  248  syl5bb  249  syl6bb  253  3bitrd  271  3bitr2d  273  3bitr3d  275  3bitr4d  277  imbi12d  312  bibi12d  313  sylan9bb  681  orbi12d  691  anbi12d  692  dedlem0a  919  3bior2fd  1291  dral1  2053  ax11el  2270  eleq12d  2503  neeq12d  2613  neleq12d  2693  raleqbi1dv  2904  rexeqbi1dv  2905  reueqd  2906  rmoeqd  2907  raleqbidv  2908  rexeqbidv  2909  raleqbidva  2910  rexeqbidva  2911  eueq3  3101  sbc19.21g  3217  sbcrext  3226  sbcabel  3230  sbcel1g  3262  sbceq1g  3263  sbcel2g  3264  sbceq2g  3265  sbccsb2g  3272  sbcco3g  3297  sseq12d  3369  psseq12d  3433  raaan  3727  raaanv  3728  sbcss  3730  elimhyp2v  3780  elimhyp4v  3782  keephyp2v  3786  ralsng  3838  rexsng  3839  ssunsn2  3950  2ralunsn  3996  csbunig  4015  disjeq12d  4183  disjprg  4200  breq123d  4218  sbcbr12g  4254  sbcbr1g  4255  sbcbr2g  4256  treq  4300  nalset  4332  copsex4g  4437  frirr  4551  ordtri1  4606  reusv7OLD  4726  reuxfr2d  4737  reuxfrd  4739  elpwun  4747  ordpwsuc  4786  ordunisuc2  4815  tfindsg  4831  dfom2  4838  findsg  4863  csbxpg  4896  posn  4937  frsn  4939  csbrng  5105  elrelimasn  5219  eliniseg  5224  brcodir  5244  fneq12d  5529  feq12d  5573  feq123d  5574  f1osng  5707  csbfv12g  5729  csbfv12gALT  5730  dmfco  5788  eqfnfv2  5819  fndmdifeq0  5827  fneqeql2  5830  funimass3  5837  funconstss  5839  unpreima  5847  ralrnmpt  5869  dffo3  5875  fmptco  5892  fressnfv  5911  fnsuppeq0  5944  fnunirn  5990  f1elima  6000  cocan1  6015  cocan2  6016  fliftf  6028  soisores  6038  isomin  6048  isoini  6049  f1oiso  6062  f1oweALT  6065  mpt2eq123dva  6126  ovid  6181  ov  6184  ovg  6203  caovord2d  6247  ofrfval2  6314  offveqb  6317  reldm  6389  mpt2xopoveq  6461  mpt2xopovel  6462  isprmpt2  6468  tpostpos  6490  f1ofveu  6575  oe0m1  6756  oaord1  6785  omord  6802  omlimcl  6812  oewordi  6825  oeeui  6836  nnaordr  6854  nnaordex  6872  ereq1  6903  brdifun  6923  erth2  6941  qliftfun  6980  brecop  6988  elmapg  7022  elpmg  7023  boxcutc  7096  dom2lem  7138  xpcomco  7189  pw2f1olem  7203  nndomo  7291  unfilem2  7363  domunfican  7370  indexfi  7405  elfi2  7410  supisolem  7464  hartogslem1  7500  brwdom2  7530  canthwdom  7536  infeq5i  7580  cantnfs  7610  cantnfrescl  7621  cantnfp1lem3  7625  cantnflem1b  7631  cantnflem1  7634  cnfcom3lem  7649  r1pwOLD  7761  rankxplim  7792  iscard2  7852  infxpenc2  7892  fseqenlem1  7894  fseqdom  7896  alephnbtwn  7941  alephinit  7965  iunfictbso  7984  dfac2  8000  dfac12lem2  8013  dfac12lem3  8014  kmlem2  8020  ackbij2lem2  8109  fin23lem23  8195  fin1a2lem2  8270  fin1a2lem4  8272  fin1a2lem9  8277  dcomex  8316  axdclem  8388  brdom7disj  8398  brdom6disj  8399  iundom2g  8404  axpownd  8465  fpwwe2cbv  8494  fpwwe2lem2  8496  fpwwe2lem3  8497  fpwwe2lem9  8502  fpwwe2  8507  pwfseqlem1  8522  eltskm  8707  ltapi  8769  ltmpi  8770  nlt1pi  8772  indpi  8773  nqereu  8795  ordpipq  8808  ltsonq  8835  ltanq  8837  ltrnq  8845  archnq  8846  elnpi  8854  genpass  8875  addclprlem1  8882  mulclprlem  8885  1idpr  8895  prlem934  8899  prlem936  8913  reclem4pr  8916  addgt0sr  8968  sqgt0sr  8970  ltresr  9004  leloe  9150  eqlelt  9151  negeu  9285  subadd2  9298  subcan2  9315  ltadd1  9484  leadd2  9486  ltsubadd  9487  lesubadd  9489  ltaddsub2  9492  leaddsub2  9494  ltaddpos  9507  lesub2  9512  ltnegcon1  9518  ltnegcon2  9519  lenegcon1  9521  lenegcon2  9522  addge01  9527  addge02  9528  suble0  9531  lesub0  9533  eqord2  9547  mulcan2d  9645  diveq0  9677  diveq1  9697  ltmul2  9850  lemul2  9852  ltmulgt11  9859  ltmulgt12  9860  gt0div  9865  ge0div  9866  ltmuldiv  9869  ledivmul2OLD  9877  ltdiv2  9884  ltrec1  9886  lerec2  9887  ledivdiv  9888  ltdiv23  9890  lediv23  9891  creur  9983  creui  9984  ofsubeq0  9986  nn1suc  10010  nnrecl  10208  nn0sub  10259  znnsub  10311  btwnnz  10335  gtndiv  10336  uzindOLD  10353  eluz2  10483  uzwo  10528  uzwoOLD  10529  indstr2  10543  negn0  10551  rpneg  10630  xrleloe  10726  xltadd2  10825  xsubge0  10829  xlesubadd  10831  xmulasslem  10853  xlemul2  10859  xltmul2  10861  supxrre2  10899  elixx3g  10918  ioo0  10930  iccid  10950  ico0  10951  ioc0  10952  icc0  10953  elioc2  10962  elico2  10963  elicc2  10964  elfz2  11039  fzen  11061  fzsubel  11077  fzpr  11090  fzrevral2  11120  fzrevral3  11121  fzshftral  11122  fzosplitsni  11184  btwnzge0  11218  mod0  11243  negmod0  11244  nn0ennn  11306  expeq0  11398  sq11  11442  sq01  11489  hashen  11619  hashnncl  11633  hashsdom  11643  seqcoll2  11701  ccatopth2  11765  cnpart  12033  sqrlem7  12042  sqrneglem  12060  sqabs  12100  abslt  12106  absle  12107  absdiflt  12109  absdifle  12110  lenegsq  12112  rexanuz2  12141  limsupgle  12259  limsuple  12260  clim  12276  rlim  12277  clim0c  12289  rlim0  12290  rlim0lt  12291  ello12  12298  ello1mpt  12303  elo12  12309  lo1o12  12315  elo1mpt  12316  elo1mpt2  12317  o1lo1  12319  isercolllem2  12447  isercoll2  12450  zsum  12500  fsum2dlem  12542  fsumcom2  12546  binomlem  12596  efieq  12752  sin01bnd  12774  cos01bnd  12775  dvdsval2  12843  dvdsaddr  12877  fzocongeq  12891  odd2np1  12896  divalglem4  12904  divalglem5  12905  divalgb  12912  bits0  12928  bitsp1e  12932  bitsp1o  12933  bitscmp  12938  bitsinv1lem  12941  sadval  12956  sadcaddlem  12957  smuval  12981  smuval2  12982  dvdssq  13048  nn0seqcvgd  13049  algcvgblem  13056  isprm2  13075  qredeq  13094  prmdvdsexp  13102  prmdvdsexpb  13103  prmexpb  13105  prmfac1  13106  qnumgt0  13130  hashdvds  13152  fermltl  13161  pcpremul  13205  pc2dvds  13240  pcz  13242  prmpwdvds  13260  prmreclem5  13276  4sqlem16  13316  vdwapun  13330  vdwmc  13334  vdwlem6  13342  ramval  13364  prdsbasmpt  13680  prdsleval  13687  prdsbasmpt2  13692  imasleval  13754  xpsle  13794  mrcidb2  13831  ismri  13844  mrieqvd  13851  acsfiel  13867  acsfn2  13876  catpropd  13923  ismon2  13948  isepi2  13955  isinv  13973  isssc  14008  subsubc  14038  funcres2b  14082  funcpropd  14085  isfull  14095  isfth  14099  fullpropd  14105  isnat2  14133  fucsect  14157  fuciso  14160  elsetchom  14224  setcsect  14232  setciso  14234  isprs  14375  isdrs  14379  posi  14395  pltval3  14412  istos  14452  islat  14464  latleeqj1  14480  latleeqj2  14481  latleeqm1  14496  latleeqm2  14497  ipodrsima  14579  isacs5  14586  acsficl2d  14590  isdlat  14607  mhmpropd  14732  issubm2  14737  gsumvalx  14762  gsumpropd  14764  grpsubrcan  14858  grplactcnv  14875  issubg  14932  eqgval  14977  conjnmzb  15028  isga  15056  odmulg  15180  odf1o1  15194  odngen  15199  gexdvds  15206  pgpfi2  15228  isslw  15230  slwpss  15234  pgpssslw  15236  subgslw  15238  sylow2alem2  15240  fislw  15247  sylow3lem2  15250  lsmelvalm  15273  lsmdisj3a  15309  pj1eq  15320  iscmn  15407  eqgabl  15442  torsubg  15457  gsumval3  15502  dprdf11  15569  dprd2da  15588  dmdprdpr  15595  ablfac1eulem  15618  pgpfac1lem2  15621  pgpfac1lem3a  15622  pgpfac1lem3  15623  rngpropd  15683  dvdsrval  15738  dvdsr02  15749  unitpropd  15790  drngmuleq0  15846  drngpropd  15850  issubrg  15856  islmod  15942  lsmelpr  16151  lspsnne1  16177  fidomndrnglem  16354  coe1mul2lem2  16649  coe1tm  16653  prmirredlem  16761  prmirred  16763  domnchr  16801  znleval  16823  znchr  16831  znunithash  16833  iscss2  16901  ishil2  16934  istopg  16956  eltg  17010  eltg2  17011  tgss2  17040  bastop1  17046  bastop2  17047  iscld  17079  iscld4  17117  elcls2  17126  elcls3  17135  isclo  17139  mretopd  17144  isnei  17155  neiint  17156  neindisj2  17175  islp2  17197  islp3  17198  maxlp  17199  cldlp  17202  neitr  17232  iscn  17287  iscnp  17289  iscnp3  17296  tgcn  17304  subbascn  17306  ssidcn  17307  lmbr2  17311  lmbrf  17312  cnnei  17334  cnrest2  17338  hausnei2  17405  cmpsub  17451  tgcmp  17452  cmpfi  17459  consuba  17471  connsub  17472  dis2ndc  17511  subislly  17532  elkgen  17556  kgencn  17576  kgencn2  17577  eltx  17588  ptpjpre1  17591  ptcnplem  17641  hausdiag  17665  xkoptsub  17674  xkoco2cn  17678  imasnopn  17710  imasncld  17711  imasncls  17712  elqtop  17717  qtopcld  17733  kqcldsat  17753  kqt0lem  17756  isr0  17757  regr1lem2  17760  ordthmeolem  17821  ptuncnv  17827  trfbas  17864  elfg  17891  trfil3  17908  trufil  17930  filufint  17940  uffix2  17944  elfm2  17968  elfm3  17970  flimtopon  17990  flimopn  17995  fbflim  17996  fbflim2  17997  flffbas  18015  flftg  18016  cnflf  18022  txflf  18026  isfcls  18029  fclstopon  18032  fclsbas  18041  fclsrest  18044  fcfnei  18055  cnfcf  18062  ptcmplem2  18072  tgphaus  18134  tgpt0  18136  divstgphaus  18140  tsmsgsum  18156  tsmsres  18161  tsmsxplem1  18170  isust  18221  elutop  18251  utopsnneiplem  18265  utopsnnei  18267  isusp  18279  isucn  18296  isucn2  18297  ucncn  18303  ispsmet  18323  ismet  18341  isxmet  18342  metn0  18378  xmetres2  18379  elbl3ps  18409  elbl3  18410  xblpnfps  18413  xblpnf  18414  elmopn2  18463  metss  18526  stdbdxmet  18533  metcnp3  18558  metcnp  18559  metcnp2  18560  metcn  18561  txmetcnp  18565  txmetcn  18566  cfilucfil2OLD  18591  cfilucfil2  18592  blval2  18593  metuelOLD  18595  metuel  18596  metuel2  18597  metucnOLD  18606  metucn  18607  dscopn  18609  isngp3  18633  nmeq0  18652  ngppropd  18666  isnghm3  18747  isnmhm2  18774  bl2ioo  18811  metdsge  18867  metnrmlem1a  18876  addcnlem  18882  elcncf  18907  elcncf2  18908  evth  18972  elpi1  19058  nmhmcn  19116  cphipeq0  19154  ipcau2  19179  lmmbr  19199  lmmbr2  19200  iscfil2  19207  fmcfil  19213  iscau2  19218  iscau3  19219  iscau4  19220  iscauf  19221  caucfil  19224  metcld2  19247  cfilucfil4OLD  19261  cfilucfil4  19262  bcthlem1  19265  lssbn  19292  cmetcusp1OLD  19293  cmetcusp1  19294  srabn  19302  ishl2  19312  minveclem7  19324  ivth2  19340  ovolfioo  19352  ovolficc  19353  ovolshftlem1  19393  ovolicc2lem1  19401  icombl  19446  ioombl  19447  volsup2  19485  ismbf  19510  ismbfcn  19511  ismbfcn2  19519  mbfmax  19529  mbfimaopnlem  19535  mbfaddlem  19540  mbfsup  19544  mbfinf  19545  mbflimsup  19546  i1faddlem  19573  i1fres  19585  itg1ge0a  19591  itg1climres  19594  mbfi1fseqlem4  19598  itg2leub  19614  itg2const  19620  itg2split  19629  itg2cnlem2  19642  iblcnlem1  19667  iblrelem  19670  itgss3  19694  ellimc  19748  ellimc2  19752  ellimc3  19754  limcmpt  19758  limcmpt2  19759  limcres  19761  cnplimc  19762  limcun  19770  dvreslem  19784  dvcnp  19793  dvcnvlem  19848  dveflem  19851  cmvth  19863  mdegleb  19975  mdegldg  19977  degltp1le  19984  mdegle0  19988  deg1ldg  20003  coe1mul3  20010  ply1remlem  20073  fta1glem2  20077  ply1termlem  20110  coemulc  20161  coecj  20184  plymul0or  20186  ofmulrt  20187  quotval  20197  plydivlem4  20201  plyremlem  20209  ulmcau2  20300  reeff1o  20351  sincosq2sgn  20395  sinq12gt0  20403  coseq1  20418  logltb  20482  cosarg0d  20492  argrege0  20494  tanarg  20502  affineequiv  20655  dcubic1lem  20671  dcubic  20674  atandm2  20705  rlimcnp  20792  rlimcnp2  20793  xrlimcnp  20795  fsumharmonic  20838  wilthlem1  20839  ftalem7  20849  basellem3  20853  isppw2  20886  issqf  20907  sqf11  20910  mumullem2  20951  sqff1o  20953  muinv  20966  ppiublem1  20974  vmasum  20988  chpchtsum  20991  chpub  20992  dchrelbas2  21009  dchrelbas3  21010  dchrelbas4  21015  dchrinv  21033  efexple  21053  bposlem1  21056  bposlem6  21061  bposlem7  21062  lgsdilem  21094  lgsdir2lem4  21098  lgsdir2  21100  lgsne0  21105  lgsabs1  21106  lgsquad3  21133  2sqlem7  21142  2sqlem8a  21143  chtppilim  21157  dchrvmaeq0  21186  dirith  21211  ostth3  21320  isumgra  21338  wrdumgra  21339  isusgra0  21364  nbgrael  21426  nbgraeledg  21430  nb3graprlem1  21448  nb3grapr2  21451  cusgra2v  21459  cusgra3vnbpr  21462  cusgrafilem3  21478  cusgrauvtxb  21493  iswlk  21515  iswlkon  21519  trls  21524  istrl  21525  istrl2  21526  istrlon  21529  ispth  21556  isspth  21557  0spth  21559  ispthon  21564  isspthon  21571  isspthonpth  21572  1pthon  21579  wlkdvspthlem  21595  0crct  21601  0cycl  21602  fargshiftfva  21614  iseupa  21675  eupatrl  21678  eupath2lem2  21688  eupath2lem3  21689  isgrpo  21772  isablo  21859  ismgm  21896  opidon2  21900  ismndo1  21920  elghomlem2  21938  iscom2  21988  rngosn3  22002  rngosn4  22003  vci  22015  isvclem  22044  vcoprnelem  22045  nvsubadd  22124  nvelbl  22173  nvelbl2  22174  nmoubi  22261  nmobndi  22264  nmoo0  22280  isph  22311  minvecolem4b  22368  minvecolem4  22370  minvecolem5  22371  minvecolem7  22373  h2hcau  22470  h2hlm  22471  hvaddeq0  22559  hial2eq2  22597  norm-i  22619  hhssnv  22752  shsel  22804  shsel3  22805  pjhtheu2  22906  chssoc  22986  chsscon1  22991  chpsscon1  22994  chpsscon2  22995  chlejb2  23003  elspansn2  23057  fh1  23108  fh2  23109  cm2j  23110  eigposi  23327  nmopub  23399  unopf1o  23407  nmfnleub  23416  elnlfn  23419  adjvalval  23428  lnopcnre  23530  riesz4i  23554  leop2  23615  leop3  23616  leoppos  23617  hst1h  23718  mdbr2  23787  mdbr3  23788  mdbr4  23789  dmdbr2  23794  dmdbr3  23796  dmdbr4  23797  mddmd2  23800  cvdmd  23828  atcvatlem  23876  atdmd  23889  sumdmdii  23906  dmdbr5ati  23913  cdj3lem1  23925  addltmulALT  23937  raleqbid  23951  rexeqbid  23952  reuxfr3d  23964  reuxfr4d  23965  iuneq12daf  23995  csbcnvg  24025  abfmpeld  24054  abfmpel  24055  fmptdF  24057  fmptcof2  24064  disjdsct  24078  xeqlelt  24127  tltnle  24178  gsumpropd2lem  24208  isofld  24223  isinftm  24239  isarchi  24240  metidv  24275  pstmxmet  24280  lmxrge0  24325  zrhker  24349  esumlub  24440  issiga  24482  dya2ub  24608  itgeq12dv  24629  orvcgteel  24713  ballotlemfc0  24738  ballotlemfcc  24739  ballotlemrv1  24766  ballotlemrv2  24767  ballotlem1ri  24780  derangval  24841  derangenlem  24845  subfacp1lem2a  24854  subfacp1lem5  24858  erdszelem8  24872  iccllyscon  24925  cvmsval  24941  untelirr  25145  untsucf  25147  untangtr  25151  mulcan2g  25178  mulle0b  25180  mulsuble0b  25181  zprod  25252  fprodcom2  25297  dfpo2  25367  dfon2lem3  25396  dfon2lem4  25397  dfon2lem7  25400  elpredim  25431  predep  25447  preduz  25455  brbtwn  25786  brcgr  25787  eqeelen  25791  brbtwn2  25792  colinearalglem1  25793  colinearalglem2  25794  colinearalglem3  25795  colinearalg  25797  axcgrid  25803  ax5seglem4  25819  ax5seglem5  25820  axbtwnid  25826  axcontlem5  25855  axcontlem7  25857  cgrcomlr  25880  ifscgr  25926  cgr3permute2  25931  cgr3permute4  25932  cgr3permute5  25933  brcolinear2  25940  brcolinear  25941  colinearperm2  25946  colinearperm4  25947  colinearperm5  25948  brofs2  25959  brifs2  25960  btwnconn1lem3  25971  btwnconn1lem4  25972  btwnconn1lem5  25973  btwnconn1lem8  25976  btwnconn1lem10  25978  btwnconn1lem11  25979  brsegle2  25991  broutsideof3  26008  outsideofeu  26013  lineunray  26029  hfninf  26075  nndivlub  26156  wl-dedlem0a  26180  ltflcei  26187  itg2addnclem2  26203  itg2addnclem3  26204  itg2gt0cn  26206  itgaddnclem2  26210  iblabsnclem  26214  dvreasin  26226  areacirclem2  26228  areacirclem5  26232  areacirclem6  26233  areacirc  26234  elicc3  26257  nn0prpwlem  26262  nn0prpw  26263  topfneec  26308  islocfin  26313  neibastop3  26328  neifg  26337  eltail  26340  filnetlem4  26347  sdclem2  26383  fdc  26386  lmclim2  26401  0totbnd  26419  sstotbnd  26421  isbnd3b  26431  ismtyval  26446  isismty  26447  ismtyima  26449  heiborlem7  26463  heiborlem10  26466  bfplem1  26468  rrnmet  26475  rrnheibor  26483  ismrer1  26484  isdrngo2  26511  isidlc  26562  ralxpxfr2d  26678  elrfi  26685  elrfirn2  26687  isnacs2  26697  mrefg3  26699  nacsfix  26703  lzunuz  26763  diophin  26768  sbc2rexg  26781  sbc4rexg  26782  sbccomieg  26786  rexrabdioph  26791  4rexfrabdioph  26795  6rexfrabdioph  26796  diophren  26811  fiphp3d  26817  irrapxlem2  26823  elpell1qr2  26872  reglogltb  26891  reglogleb  26892  monotuz  26941  monotoddzz  26943  zindbi  26946  rmyeq0  26955  jm2.19lem2  26998  jm2.19lem3  26999  rmydioph  27022  expdiophlem1  27029  expdioph  27031  pw2f1o2val2  27048  soeq12d  27049  freq12d  27050  weeq12d  27051  fnwe2lem2  27063  islmodfg  27082  islssfg2  27084  dsmmelbas  27120  ellspd  27169  pwfi2f1o  27175  islindf  27197  islbs4  27217  islinds3  27219  islnr3  27234  rngunsnply  27293  f1omvdconj  27304  f1otrspeq  27305  pmtrmvd  27313  idomrootle  27426  caofcan  27455  pm14.122c  27539  pm14.123c  27542  sbaniota  27550  fnchoice  27614  rfcnpre3  27618  rfcnpre4  27619  climinf  27646  stoweidlem7  27670  stoweidlem27  27690  stoweidlem35  27698  sbcrel  27895  csbdmg  27896  sbcfun  27901  dfdfat2  27909  fnbrafvb  27932  afvelrnb  27941  dmfcoafv  27953  otthg  28000  f12dfv  28011  f13dfv  28012  ubmelm1fzo  28039  wrdeq0  28083  modprm1div  28108  modprminveq  28110  shwrdidxmod  28131  shwrdsiun  28172  usgra2pth  28185  usgra2pth0  28186  el2wlkonot  28210  el2spthonot  28211  el2spthonot0  28212  el2wlkonotot1  28215  el2wlksotot  28223  usg2wlkonot  28224  usg2wotspth  28225  2spontn0vne  28228  usg2spthonot0  28230  usg2spthonot1  28231  2spot2iun2spont  28232  frgra3v  28250  frgrancvvdeqlem3  28279  frgrawopreglem2  28292  usg2spot2nb  28312  usgreg2spot  28314  trsbc  28480  sbcssOLD  28482  bnj984  29177  bnj1417  29264  islshpsm  29617  lrelat  29651  islshpat  29654  islshpcv  29690  ellkr  29726  lkr0f  29731  lkrsc  29734  lshpkrlem1  29747  islshpkrN  29757  lfl1dim  29758  lkrpssN  29800  ldual1dim  29803  ople0  29824  opltn0  29827  op1le  29829  opcon2b  29834  oplecon1b  29838  opltcon1b  29842  opltcon2b  29843  cmtvalN  29848  omllaw4  29883  cmt4N  29889  cmtbr3N  29891  cmtbr4N  29892  omlfh1N  29895  cvrval  29906  pats  29922  leatb  29929  atlle0  29942  atlltn0  29943  cvlatcvr1  29978  cvlatcvr2  29979  ishlat1  29989  glbconxN  30014  hlsupr2  30023  hlateq  30035  hlrelat  30038  hlrelat2  30039  cvrval5  30051  cvrexchlem  30055  atcvr0eq  30062  cvrat4  30079  3dim0  30093  3dim2  30104  2dim  30106  islln3  30146  llnexatN  30157  islpln3  30169  islpln5  30171  islvol3  30212  islvol5  30215  4atlem11  30245  4atlem12  30248  lineset  30374  psubspset  30380  ispsubsp2  30382  elpmapat  30400  pmapglbx  30405  isline3  30412  isline4N  30413  elpaddat  30440  elpadd2at  30442  pmapjoin  30488  dalawlem13  30519  ispsubcl2N  30583  lhpoc  30650  lhpmod2i2  30674  lhpmod6i1  30675  lautset  30718  pautsetN  30734  ltrnatb  30773  ltrnel  30775  ltrncnvel  30778  ltrneq  30785  trlid0b  30814  cdleme0ex2N  30860  cdleme3  30873  cdleme7  30885  cdlemefrs29bpre0  31032  cdlemg2cN  31225  cdlemg2cex  31227  cdlemk34  31546  cdlemkid3N  31569  cdlemkid4  31570  cdlemk39s  31575  cdlemk42  31577  dvhb1dimN  31622  diaord  31684  dia11N  31685  diaglbN  31692  dia1dim2  31699  dvhopellsm  31754  dibelval3  31784  dibopelval3  31785  dibeldmN  31795  dib11N  31797  dib1dim  31802  diblsmopel  31808  diclspsn  31831  dihopelvalbN  31875  dihopelvalcqat  31883  dihopelvalcpre  31885  xihopellsmN  31891  dihopellsm  31892  dihord3  31894  dihord4  31895  dih11  31902  dihglbcpreN  31937  dihmeetlem4preN  31943  dihlspsnat  31970  dihatexv2  31976  dochord2N  32008  dochord3  32009  dochkrshp2  32024  dihjatcclem4  32058  dihjat1lem  32065  dvh2dimatN  32077  lcfl2  32130  lcfl3  32131  lcfl4N  32132  lcfl7N  32138  lcfrvalsnN  32178  lcfrlem9  32187  lcdlss  32256  mapdordlem2  32274  mapd1o  32285  mapdcv  32297  mapdn0  32306  mapdindp  32308  mapdpglem3  32312  mapdpglem26  32335  mapdpglem27  32336  mapdpglem30  32339  mapdindp1  32357  lspindp5  32407  hdmap1ffval  32433  hdmap1fval  32434  hdmapffval  32466  hdmapfval  32467  hdmapeq0  32484  hdmap11  32488  hgmapffval  32525  hgmapfval  32526  hdmapoc  32571  hlhilphllem  32599
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 178
  Copyright terms: Public domain W3C validator