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  2022  ax11el  2244  eleq12d  2472  neeq12d  2582  neleq12d  2662  raleqbi1dv  2872  rexeqbi1dv  2873  reueqd  2874  rmoeqd  2875  raleqbidv  2876  rexeqbidv  2877  raleqbidva  2878  rexeqbidva  2879  eueq3  3069  sbc19.21g  3185  sbcrext  3194  sbcabel  3198  sbcel1g  3230  sbceq1g  3231  sbcel2g  3232  sbceq2g  3233  sbccsb2g  3240  sbcco3g  3265  sseq12d  3337  psseq12d  3401  raaan  3695  raaanv  3696  sbcss  3698  elimhyp2v  3748  elimhyp4v  3750  keephyp2v  3754  ralsng  3806  rexsng  3807  ssunsn2  3918  2ralunsn  3964  csbunig  3983  disjeq12d  4151  disjprg  4168  breq123d  4186  sbcbr12g  4222  sbcbr1g  4223  sbcbr2g  4224  treq  4268  nalset  4300  copsex4g  4405  frirr  4519  ordtri1  4574  reusv7OLD  4694  reuxfr2d  4705  reuxfrd  4707  elpwun  4715  ordpwsuc  4754  ordunisuc2  4783  tfindsg  4799  dfom2  4806  findsg  4831  csbxpg  4864  posn  4905  frsn  4907  csbrng  5073  elrelimasn  5187  eliniseg  5192  brcodir  5212  fneq12d  5497  feq12d  5541  feq123d  5542  f1osng  5675  csbfv12g  5697  csbfv12gALT  5698  dmfco  5756  eqfnfv2  5787  fndmdifeq0  5795  fneqeql2  5798  funimass3  5805  funconstss  5807  unpreima  5815  ralrnmpt  5837  dffo3  5843  fmptco  5860  fressnfv  5879  fnsuppeq0  5912  fnunirn  5958  f1elima  5968  cocan1  5983  cocan2  5984  fliftf  5996  soisores  6006  isomin  6016  isoini  6017  f1oiso  6030  f1oweALT  6033  mpt2eq123dva  6094  ovid  6149  ov  6152  ovg  6171  caovord2d  6215  ofrfval2  6282  offveqb  6285  reldm  6357  mpt2xopoveq  6429  mpt2xopovel  6430  isprmpt2  6436  tpostpos  6458  f1ofveu  6543  oe0m1  6724  oaord1  6753  omord  6770  omlimcl  6780  oewordi  6793  oeeui  6804  nnaordr  6822  nnaordex  6840  ereq1  6871  brdifun  6891  erth2  6909  qliftfun  6948  brecop  6956  elmapg  6990  elpmg  6991  boxcutc  7064  dom2lem  7106  xpcomco  7157  pw2f1olem  7171  nndomo  7259  unfilem2  7331  domunfican  7338  indexfi  7372  elfi2  7377  supisolem  7431  hartogslem1  7467  brwdom2  7497  canthwdom  7503  infeq5i  7547  cantnfs  7577  cantnfrescl  7588  cantnfp1lem3  7592  cantnflem1b  7598  cantnflem1  7601  cnfcom3lem  7616  r1pwOLD  7728  rankxplim  7759  iscard2  7819  infxpenc2  7859  fseqenlem1  7861  fseqdom  7863  alephnbtwn  7908  alephinit  7932  iunfictbso  7951  dfac2  7967  dfac12lem2  7980  dfac12lem3  7981  kmlem2  7987  ackbij2lem2  8076  fin23lem23  8162  fin1a2lem2  8237  fin1a2lem4  8239  fin1a2lem9  8244  dcomex  8283  axdclem  8355  brdom7disj  8365  brdom6disj  8366  iundom2g  8371  axpownd  8432  fpwwe2cbv  8461  fpwwe2lem2  8463  fpwwe2lem3  8464  fpwwe2lem9  8469  fpwwe2  8474  pwfseqlem1  8489  eltskm  8674  ltapi  8736  ltmpi  8737  nlt1pi  8739  indpi  8740  nqereu  8762  ordpipq  8775  ltsonq  8802  ltanq  8804  ltrnq  8812  archnq  8813  elnpi  8821  genpass  8842  addclprlem1  8849  mulclprlem  8852  1idpr  8862  prlem934  8866  prlem936  8880  reclem4pr  8883  addgt0sr  8935  sqgt0sr  8937  ltresr  8971  leloe  9117  eqlelt  9118  negeu  9252  subadd2  9265  subcan2  9282  ltadd1  9451  leadd2  9453  ltsubadd  9454  lesubadd  9456  ltaddsub2  9459  leaddsub2  9461  ltaddpos  9474  lesub2  9479  ltnegcon1  9485  ltnegcon2  9486  lenegcon1  9488  lenegcon2  9489  addge01  9494  addge02  9495  suble0  9498  lesub0  9500  eqord2  9514  mulcan2d  9612  diveq0  9644  diveq1  9664  ltmul2  9817  lemul2  9819  ltmulgt11  9826  ltmulgt12  9827  gt0div  9832  ge0div  9833  ltmuldiv  9836  ledivmul2OLD  9844  ltdiv2  9851  ltrec1  9853  lerec2  9854  ledivdiv  9855  ltdiv23  9857  lediv23  9858  creur  9950  creui  9951  ofsubeq0  9953  nn1suc  9977  nnrecl  10175  nn0sub  10226  znnsub  10278  btwnnz  10302  gtndiv  10303  uzindOLD  10320  eluz2  10450  uzwo  10495  uzwoOLD  10496  indstr2  10510  negn0  10518  rpneg  10597  xrleloe  10693  xltadd2  10792  xsubge0  10796  xlesubadd  10798  xmulasslem  10820  xlemul2  10826  xltmul2  10828  supxrre2  10866  elixx3g  10885  ioo0  10897  iccid  10917  ico0  10918  ioc0  10919  icc0  10920  elioc2  10929  elico2  10930  elicc2  10931  elfz2  11006  fzen  11028  fzsubel  11044  fzpr  11057  fzrevral2  11087  fzrevral3  11088  fzshftral  11089  fzosplitsni  11151  btwnzge0  11185  mod0  11210  negmod0  11211  nn0ennn  11273  expeq0  11365  sq11  11409  sq01  11456  hashen  11586  hashnncl  11600  hashsdom  11610  seqcoll2  11668  ccatopth2  11732  cnpart  12000  sqrlem7  12009  sqrneglem  12027  sqabs  12067  abslt  12073  absle  12074  absdiflt  12076  absdifle  12077  lenegsq  12079  rexanuz2  12108  limsupgle  12226  limsuple  12227  clim  12243  rlim  12244  clim0c  12256  rlim0  12257  rlim0lt  12258  ello12  12265  ello1mpt  12270  elo12  12276  lo1o12  12282  elo1mpt  12283  elo1mpt2  12284  o1lo1  12286  isercolllem2  12414  isercoll2  12417  zsum  12467  fsum2dlem  12509  fsumcom2  12513  binomlem  12563  efieq  12719  sin01bnd  12741  cos01bnd  12742  dvdsval2  12810  dvdsaddr  12844  fzocongeq  12858  odd2np1  12863  divalglem4  12871  divalglem5  12872  divalgb  12879  bits0  12895  bitsp1e  12899  bitsp1o  12900  bitscmp  12905  bitsinv1lem  12908  sadval  12923  sadcaddlem  12924  smuval  12948  smuval2  12949  dvdssq  13015  nn0seqcvgd  13016  algcvgblem  13023  isprm2  13042  qredeq  13061  prmdvdsexp  13069  prmdvdsexpb  13070  prmexpb  13072  prmfac1  13073  qnumgt0  13097  hashdvds  13119  fermltl  13128  pcpremul  13172  pc2dvds  13207  pcz  13209  prmpwdvds  13227  prmreclem5  13243  4sqlem16  13283  vdwapun  13297  vdwmc  13301  vdwlem6  13309  ramval  13331  prdsbasmpt  13647  prdsleval  13654  prdsbasmpt2  13659  imasleval  13721  xpsle  13761  mrcidb2  13798  ismri  13811  mrieqvd  13818  acsfiel  13834  acsfn2  13843  catpropd  13890  ismon2  13915  isepi2  13922  isinv  13940  isssc  13975  subsubc  14005  funcres2b  14049  funcpropd  14052  isfull  14062  isfth  14066  fullpropd  14072  isnat2  14100  fucsect  14124  fuciso  14127  elsetchom  14191  setcsect  14199  setciso  14201  isprs  14342  isdrs  14346  posi  14362  pltval3  14379  istos  14419  islat  14431  latleeqj1  14447  latleeqj2  14448  latleeqm1  14463  latleeqm2  14464  ipodrsima  14546  isacs5  14553  acsficl2d  14557  isdlat  14574  mhmpropd  14699  issubm2  14704  gsumvalx  14729  gsumpropd  14731  grpsubrcan  14825  grplactcnv  14842  issubg  14899  eqgval  14944  conjnmzb  14995  isga  15023  odmulg  15147  odf1o1  15161  odngen  15166  gexdvds  15173  pgpfi2  15195  isslw  15197  slwpss  15201  pgpssslw  15203  subgslw  15205  sylow2alem2  15207  fislw  15214  sylow3lem2  15217  lsmelvalm  15240  lsmdisj3a  15276  pj1eq  15287  iscmn  15374  eqgabl  15409  torsubg  15424  gsumval3  15469  dprdf11  15536  dprd2da  15555  dmdprdpr  15562  ablfac1eulem  15585  pgpfac1lem2  15588  pgpfac1lem3a  15589  pgpfac1lem3  15590  rngpropd  15650  dvdsrval  15705  dvdsr02  15716  unitpropd  15757  drngmuleq0  15813  drngpropd  15817  issubrg  15823  islmod  15909  lsmelpr  16118  lspsnne1  16144  fidomndrnglem  16321  coe1mul2lem2  16616  coe1tm  16620  prmirredlem  16728  prmirred  16730  domnchr  16768  znleval  16790  znchr  16798  znunithash  16800  iscss2  16868  ishil2  16901  istopg  16923  eltg  16977  eltg2  16978  tgss2  17007  bastop1  17013  bastop2  17014  iscld  17046  iscld4  17084  elcls2  17093  elcls3  17102  isclo  17106  mretopd  17111  isnei  17122  neiint  17123  neindisj2  17142  islp2  17164  maxlp  17165  cldlp  17168  neitr  17198  iscn  17253  iscnp  17255  iscnp3  17262  tgcn  17270  subbascn  17272  ssidcn  17273  lmbr2  17277  lmbrf  17278  cnnei  17300  cnrest2  17304  hausnei2  17371  cmpsub  17417  tgcmp  17418  cmpfi  17425  consuba  17436  connsub  17437  dis2ndc  17476  subislly  17497  elkgen  17521  kgencn  17541  kgencn2  17542  eltx  17553  ptpjpre1  17556  ptcnplem  17606  hausdiag  17630  xkoptsub  17639  xkoco2cn  17643  imasnopn  17675  imasncld  17676  imasncls  17677  elqtop  17682  qtopcld  17698  kqcldsat  17718  kqt0lem  17721  isr0  17722  regr1lem2  17725  ordthmeolem  17786  ptuncnv  17792  trfbas  17829  elfg  17856  trfil3  17873  trufil  17895  filufint  17905  uffix2  17909  elfm2  17933  elfm3  17935  flimtopon  17955  flimopn  17960  fbflim  17961  fbflim2  17962  flffbas  17980  flftg  17981  cnflf  17987  txflf  17991  isfcls  17994  fclstopon  17997  fclsbas  18006  fclsrest  18009  fcfnei  18020  cnfcf  18027  ptcmplem2  18037  tgphaus  18099  tgpt0  18101  divstgphaus  18105  tsmsgsum  18121  tsmsres  18126  tsmsxplem1  18135  isust  18186  elutop  18216  utopsnneiplem  18230  utopsnnei  18232  isusp  18244  isucn  18261  isucn2  18262  ucncn  18268  ispsmet  18288  ismet  18306  isxmet  18307  metn0  18343  xmetres2  18344  elbl3ps  18374  elbl3  18375  xblpnfps  18378  xblpnf  18379  elmopn2  18428  metss  18491  stdbdxmet  18498  metcnp3  18523  metcnp  18524  metcnp2  18525  metcn  18526  txmetcnp  18530  txmetcn  18531  cfilucfil2OLD  18556  cfilucfil2  18557  blval2  18558  metuelOLD  18560  metuel  18561  metuel2  18562  metucnOLD  18571  metucn  18572  dscopn  18574  isngp3  18598  nmeq0  18617  ngppropd  18631  isnghm3  18712  isnmhm2  18739  bl2ioo  18776  metdsge  18832  metnrmlem1a  18841  addcnlem  18847  elcncf  18872  elcncf2  18873  evth  18937  elpi1  19023  nmhmcn  19081  cphipeq0  19119  ipcau2  19144  lmmbr  19164  lmmbr2  19165  iscfil2  19172  fmcfil  19178  iscau2  19183  iscau3  19184  iscau4  19185  iscauf  19186  caucfil  19189  metcld2  19212  cfilucfil4OLD  19226  cfilucfil4  19227  bcthlem1  19230  lssbn  19257  cmetcusp1OLD  19258  cmetcusp1  19259  srabn  19267  ishl2  19277  minveclem7  19289  ivth2  19305  ovolfioo  19317  ovolficc  19318  ovolshftlem1  19358  ovolicc2lem1  19366  icombl  19411  ioombl  19412  volsup2  19450  ismbf  19475  ismbfcn  19476  ismbfcn2  19484  mbfmax  19494  mbfimaopnlem  19500  mbfaddlem  19505  mbfsup  19509  mbfinf  19510  mbflimsup  19511  i1faddlem  19538  i1fres  19550  itg1ge0a  19556  itg1climres  19559  mbfi1fseqlem4  19563  itg2leub  19579  itg2const  19585  itg2split  19594  itg2cnlem2  19607  iblcnlem1  19632  iblrelem  19635  itgss3  19659  ellimc  19713  ellimc2  19717  ellimc3  19719  limcmpt  19723  limcmpt2  19724  limcres  19726  cnplimc  19727  limcun  19735  dvreslem  19749  dvcnp  19758  dvcnvlem  19813  dveflem  19816  cmvth  19828  mdegleb  19940  mdegldg  19942  degltp1le  19949  mdegle0  19953  deg1ldg  19968  coe1mul3  19975  ply1remlem  20038  fta1glem2  20042  ply1termlem  20075  coemulc  20126  coecj  20149  plymul0or  20151  ofmulrt  20152  quotval  20162  plydivlem4  20166  plyremlem  20174  ulmcau2  20265  reeff1o  20316  sincosq2sgn  20360  sinq12gt0  20368  coseq1  20383  logltb  20447  cosarg0d  20457  argrege0  20459  tanarg  20467  affineequiv  20620  dcubic1lem  20636  dcubic  20639  atandm2  20670  rlimcnp  20757  rlimcnp2  20758  xrlimcnp  20760  fsumharmonic  20803  wilthlem1  20804  ftalem7  20814  basellem3  20818  isppw2  20851  issqf  20872  sqf11  20875  mumullem2  20916  sqff1o  20918  muinv  20931  ppiublem1  20939  vmasum  20953  chpchtsum  20956  chpub  20957  dchrelbas2  20974  dchrelbas3  20975  dchrelbas4  20980  dchrinv  20998  efexple  21018  bposlem1  21021  bposlem6  21026  bposlem7  21027  lgsdilem  21059  lgsdir2lem4  21063  lgsdir2  21065  lgsne0  21070  lgsabs1  21071  lgsquad3  21098  2sqlem7  21107  2sqlem8a  21108  chtppilim  21122  dchrvmaeq0  21151  dirith  21176  ostth3  21285  isumgra  21303  wrdumgra  21304  isusgra0  21329  nbgrael  21391  nbgraeledg  21395  nb3graprlem1  21413  nb3grapr2  21416  cusgra2v  21424  cusgra3vnbpr  21427  cusgrafilem3  21443  cusgrauvtxb  21458  iswlk  21480  iswlkon  21484  trls  21489  istrl  21490  istrl2  21491  istrlon  21494  ispth  21521  isspth  21522  0spth  21524  ispthon  21529  isspthon  21536  isspthonpth  21537  1pthon  21544  wlkdvspthlem  21560  0crct  21566  0cycl  21567  fargshiftfva  21579  iseupa  21640  eupatrl  21643  eupath2lem2  21653  eupath2lem3  21654  isgrpo  21737  isablo  21824  ismgm  21861  opidon2  21865  ismndo1  21885  elghomlem2  21903  iscom2  21953  rngosn3  21967  rngosn4  21968  vci  21980  isvclem  22009  vcoprnelem  22010  nvsubadd  22089  nvelbl  22138  nvelbl2  22139  nmoubi  22226  nmobndi  22229  nmoo0  22245  isph  22276  minvecolem4b  22333  minvecolem4  22335  minvecolem5  22336  minvecolem7  22338  h2hcau  22435  h2hlm  22436  hvaddeq0  22524  hial2eq2  22562  norm-i  22584  hhssnv  22717  shsel  22769  shsel3  22770  pjhtheu2  22871  chssoc  22951  chsscon1  22956  chpsscon1  22959  chpsscon2  22960  chlejb2  22968  elspansn2  23022  fh1  23073  fh2  23074  cm2j  23075  eigposi  23292  nmopub  23364  unopf1o  23372  nmfnleub  23381  elnlfn  23384  adjvalval  23393  lnopcnre  23495  riesz4i  23519  leop2  23580  leop3  23581  leoppos  23582  hst1h  23683  mdbr2  23752  mdbr3  23753  mdbr4  23754  dmdbr2  23759  dmdbr3  23761  dmdbr4  23762  mddmd2  23765  cvdmd  23793  atcvatlem  23841  atdmd  23854  sumdmdii  23871  dmdbr5ati  23878  cdj3lem1  23890  addltmulALT  23902  raleqbid  23916  rexeqbid  23917  reuxfr3d  23929  reuxfr4d  23930  iuneq12daf  23960  csbcnvg  23990  abfmpeld  24019  abfmpel  24020  fmptdF  24022  fmptcof2  24029  disjdsct  24043  xeqlelt  24092  tltnle  24143  gsumpropd2lem  24173  isofld  24188  isinftm  24204  isarchi  24205  metidv  24240  pstmxmet  24245  lmxrge0  24290  zrhker  24314  esumlub  24405  issiga  24447  dya2ub  24573  itgeq12dv  24594  orvcgteel  24678  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemrv1  24731  ballotlemrv2  24732  ballotlem1ri  24745  derangval  24806  derangenlem  24810  subfacp1lem2a  24819  subfacp1lem5  24823  erdszelem8  24837  iccllyscon  24890  cvmsval  24906  untelirr  25110  untsucf  25112  untangtr  25116  mulcan2g  25143  mulle0b  25145  mulsuble0b  25146  zprod  25216  fprodcom2  25261  dfpo2  25326  dfon2lem3  25355  dfon2lem4  25356  dfon2lem7  25359  elpredim  25390  predep  25406  preduz  25414  brbtwn  25742  brcgr  25743  eqeelen  25747  brbtwn2  25748  colinearalglem1  25749  colinearalglem2  25750  colinearalglem3  25751  colinearalg  25753  axcgrid  25759  ax5seglem4  25775  ax5seglem5  25776  axbtwnid  25782  axcontlem5  25811  axcontlem7  25813  cgrcomlr  25836  ifscgr  25882  cgr3permute2  25887  cgr3permute4  25888  cgr3permute5  25889  brcolinear2  25896  brcolinear  25897  colinearperm2  25902  colinearperm4  25903  colinearperm5  25904  brofs2  25915  brifs2  25916  btwnconn1lem3  25927  btwnconn1lem4  25928  btwnconn1lem5  25929  btwnconn1lem8  25932  btwnconn1lem10  25934  btwnconn1lem11  25935  brsegle2  25947  broutsideof3  25964  outsideofeu  25969  lineunray  25985  hfninf  26031  nndivlub  26112  wl-dedlem0a  26136  ltflcei  26140  itg2addnclem2  26156  itg2addnclem3  26157  itg2gt0cn  26159  itgaddnclem2  26163  iblabsnclem  26167  dvreasin  26179  areacirclem2  26181  areacirclem5  26185  areacirclem6  26186  areacirc  26187  elicc3  26210  nn0prpwlem  26215  nn0prpw  26216  topfneec  26261  islocfin  26266  neibastop3  26281  neifg  26290  eltail  26293  filnetlem4  26300  sdclem2  26336  fdc  26339  lmclim2  26354  0totbnd  26372  sstotbnd  26374  isbnd3b  26384  ismtyval  26399  isismty  26400  ismtyima  26402  heiborlem7  26416  heiborlem10  26419  bfplem1  26421  rrnmet  26428  rrnheibor  26436  ismrer1  26437  isdrngo2  26464  isidlc  26515  ralxpxfr2d  26631  elrfi  26638  elrfirn2  26640  isnacs2  26650  mrefg3  26652  nacsfix  26656  lzunuz  26716  diophin  26721  sbc2rexg  26734  sbc4rexg  26735  sbccomieg  26739  rexrabdioph  26744  4rexfrabdioph  26748  6rexfrabdioph  26749  diophren  26764  fiphp3d  26770  irrapxlem2  26776  elpell1qr2  26825  reglogltb  26844  reglogleb  26845  monotuz  26894  monotoddzz  26896  zindbi  26899  rmyeq0  26908  jm2.19lem2  26951  jm2.19lem3  26952  rmydioph  26975  expdiophlem1  26982  expdioph  26984  pw2f1o2val2  27001  soeq12d  27002  freq12d  27003  weeq12d  27004  fnwe2lem2  27016  islmodfg  27035  islssfg2  27037  dsmmelbas  27073  ellspd  27122  pwfi2f1o  27128  islindf  27150  islbs4  27170  islinds3  27172  islnr3  27187  rngunsnply  27246  f1omvdconj  27257  f1otrspeq  27258  pmtrmvd  27266  idomrootle  27379  caofcan  27408  pm14.122c  27492  pm14.123c  27495  sbaniota  27503  fnchoice  27567  rfcnpre3  27571  rfcnpre4  27572  climinf  27599  stoweidlem7  27623  stoweidlem27  27643  stoweidlem35  27651  sbcrel  27848  csbdmg  27849  sbcfun  27854  dfdfat2  27862  fnbrafvb  27885  afvelrnb  27894  dmfcoafv  27906  otthg  27952  f12dfv  27961  f13dfv  27962  ubmelm1fzo  27987  usgra2pth  28041  usgra2pth0  28042  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  el2wlkonotot1  28071  el2wlksotot  28079  usg2wlkonot  28080  usg2wotspth  28081  2spontn0vne  28084  usg2spthonot0  28086  usg2spthonot1  28087  2spot2iun2spont  28088  frgra3v  28106  frgrancvvdeqlem3  28135  frgrawopreglem2  28148  usg2spot2nb  28168  usgreg2spot  28170  trsbc  28336  sbcssOLD  28338  bnj984  29029  bnj1417  29116  islshpsm  29463  lrelat  29497  islshpat  29500  islshpcv  29536  ellkr  29572  lkr0f  29577  lkrsc  29580  lshpkrlem1  29593  islshpkrN  29603  lfl1dim  29604  lkrpssN  29646  ldual1dim  29649  ople0  29670  opltn0  29673  op1le  29675  opcon2b  29680  oplecon1b  29684  opltcon1b  29688  opltcon2b  29689  cmtvalN  29694  omllaw4  29729  cmt4N  29735  cmtbr3N  29737  cmtbr4N  29738  omlfh1N  29741  cvrval  29752  pats  29768  leatb  29775  atlle0  29788  atlltn0  29789  cvlatcvr1  29824  cvlatcvr2  29825  ishlat1  29835  glbconxN  29860  hlsupr2  29869  hlateq  29881  hlrelat  29884  hlrelat2  29885  cvrval5  29897  cvrexchlem  29901  atcvr0eq  29908  cvrat4  29925  3dim0  29939  3dim2  29950  2dim  29952  islln3  29992  llnexatN  30003  islpln3  30015  islpln5  30017  islvol3  30058  islvol5  30061  4atlem11  30091  4atlem12  30094  lineset  30220  psubspset  30226  ispsubsp2  30228  elpmapat  30246  pmapglbx  30251  isline3  30258  isline4N  30259  elpaddat  30286  elpadd2at  30288  pmapjoin  30334  dalawlem13  30365  ispsubcl2N  30429  lhpoc  30496  lhpmod2i2  30520  lhpmod6i1  30521  lautset  30564  pautsetN  30580  ltrnatb  30619  ltrnel  30621  ltrncnvel  30624  ltrneq  30631  trlid0b  30660  cdleme0ex2N  30706  cdleme3  30719  cdleme7  30731  cdlemefrs29bpre0  30878  cdlemg2cN  31071  cdlemg2cex  31073  cdlemk34  31392  cdlemkid3N  31415  cdlemkid4  31416  cdlemk39s  31421  cdlemk42  31423  dvhb1dimN  31468  diaord  31530  dia11N  31531  diaglbN  31538  dia1dim2  31545  dvhopellsm  31600  dibelval3  31630  dibopelval3  31631  dibeldmN  31641  dib11N  31643  dib1dim  31648  diblsmopel  31654  diclspsn  31677  dihopelvalbN  31721  dihopelvalcqat  31729  dihopelvalcpre  31731  xihopellsmN  31737  dihopellsm  31738  dihord3  31740  dihord4  31741  dih11  31748  dihglbcpreN  31783  dihmeetlem4preN  31789  dihlspsnat  31816  dihatexv2  31822  dochord2N  31854  dochord3  31855  dochkrshp2  31870  dihjatcclem4  31904  dihjat1lem  31911  dvh2dimatN  31923  lcfl2  31976  lcfl3  31977  lcfl4N  31978  lcfl7N  31984  lcfrvalsnN  32024  lcfrlem9  32033  lcdlss  32102  mapdordlem2  32120  mapd1o  32131  mapdcv  32143  mapdn0  32152  mapdindp  32154  mapdpglem3  32158  mapdpglem26  32181  mapdpglem27  32182  mapdpglem30  32185  mapdindp1  32203  lspindp5  32253  hdmap1ffval  32279  hdmap1fval  32280  hdmapffval  32312  hdmapfval  32313  hdmapeq0  32330  hdmap11  32334  hgmapffval  32371  hgmapfval  32372  hdmapoc  32417  hlhilphllem  32445
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