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  2058  ax11el  2273  eleq12d  2506  neeq12d  2618  neleq12d  2703  raleqbi1dv  2914  rexeqbi1dv  2915  reueqd  2916  rmoeqd  2917  raleqbidv  2918  rexeqbidv  2919  raleqbidva  2920  rexeqbidva  2921  eueq3  3111  sbc19.21g  3227  sbcrext  3236  sbcabel  3240  sbcel1g  3272  sbceq1g  3273  sbcel2g  3274  sbceq2g  3275  sbccsb2g  3282  sbcco3g  3307  sseq12d  3379  psseq12d  3443  raaan  3737  raaanv  3738  sbcss  3740  elimhyp2v  3790  elimhyp4v  3792  keephyp2v  3796  ralsng  3848  rexsng  3849  ssunsn2  3960  2ralunsn  4006  csbunig  4025  disjeq12d  4194  disjprg  4211  breq123d  4229  sbcbr12g  4265  sbcbr1g  4266  sbcbr2g  4267  treq  4311  nalset  4343  copsex4g  4448  frirr  4562  ordtri1  4617  reusv7OLD  4738  reuxfr2d  4749  reuxfrd  4751  elpwun  4759  ordpwsuc  4798  ordunisuc2  4827  tfindsg  4843  dfom2  4850  findsg  4875  csbxpg  4908  posn  4949  frsn  4951  csbrng  5117  elrelimasn  5231  eliniseg  5236  brcodir  5256  fneq12d  5541  feq12d  5585  feq123d  5586  f1osng  5719  csbfv12g  5741  csbfv12gALT  5742  dmfco  5800  eqfnfv2  5831  fndmdifeq0  5839  fneqeql2  5842  funimass3  5849  funconstss  5851  unpreima  5859  ralrnmpt  5881  dffo3  5887  fmptco  5904  fressnfv  5923  fnsuppeq0  5956  fnunirn  6002  f1elima  6012  cocan1  6027  cocan2  6028  fliftf  6040  soisores  6050  isomin  6060  isoini  6061  f1oiso  6074  f1oweALT  6077  mpt2eq123dva  6138  ovid  6193  ov  6196  ovg  6215  caovord2d  6259  ofrfval2  6326  offveqb  6329  reldm  6401  mpt2xopoveq  6473  mpt2xopovel  6474  isprmpt2  6480  tpostpos  6502  f1ofveu  6587  oe0m1  6768  oaord1  6797  omord  6814  omlimcl  6824  oewordi  6837  oeeui  6848  nnaordr  6866  nnaordex  6884  ereq1  6915  brdifun  6935  erth2  6953  qliftfun  6992  brecop  7000  elmapg  7034  elpmg  7035  boxcutc  7108  dom2lem  7150  xpcomco  7201  pw2f1olem  7215  nndomo  7303  unfilem2  7375  domunfican  7382  indexfi  7417  elfi2  7422  supisolem  7478  hartogslem1  7514  brwdom2  7544  canthwdom  7550  infeq5i  7594  cantnfs  7624  cantnfrescl  7635  cantnfp1lem3  7639  cantnflem1b  7645  cantnflem1  7648  cnfcom3lem  7663  r1pwOLD  7775  rankxplim  7808  iscard2  7868  infxpenc2  7908  fseqenlem1  7910  fseqdom  7912  alephnbtwn  7957  alephinit  7981  iunfictbso  8000  dfac2  8016  dfac12lem2  8029  dfac12lem3  8030  kmlem2  8036  ackbij2lem2  8125  fin23lem23  8211  fin1a2lem2  8286  fin1a2lem4  8288  fin1a2lem9  8293  dcomex  8332  axdclem  8404  brdom7disj  8414  brdom6disj  8415  iundom2g  8420  axpownd  8481  fpwwe2cbv  8510  fpwwe2lem2  8512  fpwwe2lem3  8513  fpwwe2lem9  8518  fpwwe2  8523  pwfseqlem1  8538  eltskm  8723  ltapi  8785  ltmpi  8786  nlt1pi  8788  indpi  8789  nqereu  8811  ordpipq  8824  ltsonq  8851  ltanq  8853  ltrnq  8861  archnq  8862  elnpi  8870  genpass  8891  addclprlem1  8898  mulclprlem  8901  1idpr  8911  prlem934  8915  prlem936  8929  reclem4pr  8932  addgt0sr  8984  sqgt0sr  8986  ltresr  9020  leloe  9166  eqlelt  9167  negeu  9301  subadd2  9314  subcan2  9331  ltadd1  9500  leadd2  9502  ltsubadd  9503  lesubadd  9505  ltaddsub2  9508  leaddsub2  9510  ltaddpos  9523  lesub2  9528  ltnegcon1  9534  ltnegcon2  9535  lenegcon1  9537  lenegcon2  9538  addge01  9543  addge02  9544  suble0  9547  lesub0  9549  eqord2  9563  mulcan2d  9661  diveq0  9693  diveq1  9713  ltmul2  9866  lemul2  9868  ltmulgt11  9875  ltmulgt12  9876  gt0div  9881  ge0div  9882  ltmuldiv  9885  ledivmul2OLD  9893  ltdiv2  9900  ltrec1  9902  lerec2  9903  ledivdiv  9904  ltdiv23  9906  lediv23  9907  creur  9999  creui  10000  ofsubeq0  10002  nn1suc  10026  nnrecl  10224  nn0sub  10275  znnsub  10327  btwnnz  10351  gtndiv  10352  uzindOLD  10369  eluz2  10499  uzwo  10544  uzwoOLD  10545  indstr2  10559  negn0  10567  rpneg  10646  xrleloe  10742  xltadd2  10841  xsubge0  10845  xlesubadd  10847  xmulasslem  10869  xlemul2  10875  xltmul2  10877  supxrre2  10915  elixx3g  10934  ioo0  10946  iccid  10966  ico0  10967  ioc0  10968  icc0  10969  elioc2  10978  elico2  10979  elicc2  10980  elfz2  11055  fzen  11077  fzsubel  11093  fzpr  11106  fzrevral2  11137  fzrevral3  11138  fzshftral  11139  fzosplitsni  11201  btwnzge0  11235  mod0  11260  negmod0  11261  nn0ennn  11323  expeq0  11415  sq11  11459  sq01  11506  hashen  11636  hashnncl  11650  hashsdom  11660  seqcoll2  11718  ccatopth2  11782  cnpart  12050  sqrlem7  12059  sqrneglem  12077  sqabs  12117  abslt  12123  absle  12124  absdiflt  12126  absdifle  12127  lenegsq  12129  rexanuz2  12158  limsupgle  12276  limsuple  12277  clim  12293  rlim  12294  clim0c  12306  rlim0  12307  rlim0lt  12308  ello12  12315  ello1mpt  12320  elo12  12326  lo1o12  12332  elo1mpt  12333  elo1mpt2  12334  o1lo1  12336  isercolllem2  12464  isercoll2  12467  zsum  12517  fsum2dlem  12559  fsumcom2  12563  binomlem  12613  efieq  12769  sin01bnd  12791  cos01bnd  12792  dvdsval2  12860  dvdsaddr  12894  fzocongeq  12908  odd2np1  12913  divalglem4  12921  divalglem5  12922  divalgb  12929  bits0  12945  bitsp1e  12949  bitsp1o  12950  bitscmp  12955  bitsinv1lem  12958  sadval  12973  sadcaddlem  12974  smuval  12998  smuval2  12999  dvdssq  13065  nn0seqcvgd  13066  algcvgblem  13073  isprm2  13092  qredeq  13111  prmdvdsexp  13119  prmdvdsexpb  13120  prmexpb  13122  prmfac1  13123  qnumgt0  13147  hashdvds  13169  fermltl  13178  pcpremul  13222  pc2dvds  13257  pcz  13259  prmpwdvds  13277  prmreclem5  13293  4sqlem16  13333  vdwapun  13347  vdwmc  13351  vdwlem6  13359  ramval  13381  prdsbasmpt  13697  prdsleval  13704  prdsbasmpt2  13709  imasleval  13771  xpsle  13811  mrcidb2  13848  ismri  13861  mrieqvd  13868  acsfiel  13884  acsfn2  13893  catpropd  13940  ismon2  13965  isepi2  13972  isinv  13990  isssc  14025  subsubc  14055  funcres2b  14099  funcpropd  14102  isfull  14112  isfth  14116  fullpropd  14122  isnat2  14150  fucsect  14174  fuciso  14177  elsetchom  14241  setcsect  14249  setciso  14251  isprs  14392  isdrs  14396  posi  14412  pltval3  14429  istos  14469  islat  14481  latleeqj1  14497  latleeqj2  14498  latleeqm1  14513  latleeqm2  14514  ipodrsima  14596  isacs5  14603  acsficl2d  14607  isdlat  14624  mhmpropd  14749  issubm2  14754  gsumvalx  14779  gsumpropd  14781  grpsubrcan  14875  grplactcnv  14892  issubg  14949  eqgval  14994  conjnmzb  15045  isga  15073  odmulg  15197  odf1o1  15211  odngen  15216  gexdvds  15223  pgpfi2  15245  isslw  15247  slwpss  15251  pgpssslw  15253  subgslw  15255  sylow2alem2  15257  fislw  15264  sylow3lem2  15267  lsmelvalm  15290  lsmdisj3a  15326  pj1eq  15337  iscmn  15424  eqgabl  15459  torsubg  15474  gsumval3  15519  dprdf11  15586  dprd2da  15605  dmdprdpr  15612  ablfac1eulem  15635  pgpfac1lem2  15638  pgpfac1lem3a  15639  pgpfac1lem3  15640  rngpropd  15700  dvdsrval  15755  dvdsr02  15766  unitpropd  15807  drngmuleq0  15863  drngpropd  15867  issubrg  15873  islmod  15959  lsmelpr  16168  lspsnne1  16194  fidomndrnglem  16371  coe1mul2lem2  16666  coe1tm  16670  prmirredlem  16778  prmirred  16780  domnchr  16818  znleval  16840  znchr  16848  znunithash  16850  iscss2  16918  ishil2  16951  istopg  16973  eltg  17027  eltg2  17028  tgss2  17057  bastop1  17063  bastop2  17064  iscld  17096  iscld4  17134  elcls2  17143  elcls3  17152  isclo  17156  mretopd  17161  isnei  17172  neiint  17173  neindisj2  17192  islp2  17214  islp3  17215  maxlp  17216  cldlp  17219  neitr  17249  iscn  17304  iscnp  17306  iscnp3  17313  tgcn  17321  subbascn  17323  ssidcn  17324  lmbr2  17328  lmbrf  17329  cnnei  17351  cnrest2  17355  hausnei2  17422  cmpsub  17468  tgcmp  17469  cmpfi  17476  consuba  17488  connsub  17489  dis2ndc  17528  subislly  17549  elkgen  17573  kgencn  17593  kgencn2  17594  eltx  17605  ptpjpre1  17608  ptcnplem  17658  hausdiag  17682  xkoptsub  17691  xkoco2cn  17695  imasnopn  17727  imasncld  17728  imasncls  17729  elqtop  17734  qtopcld  17750  kqcldsat  17770  kqt0lem  17773  isr0  17774  regr1lem2  17777  ordthmeolem  17838  ptuncnv  17844  trfbas  17881  elfg  17908  trfil3  17925  trufil  17947  filufint  17957  uffix2  17961  elfm2  17985  elfm3  17987  flimtopon  18007  flimopn  18012  fbflim  18013  fbflim2  18014  flffbas  18032  flftg  18033  cnflf  18039  txflf  18043  isfcls  18046  fclstopon  18049  fclsbas  18058  fclsrest  18061  fcfnei  18072  cnfcf  18079  ptcmplem2  18089  tgphaus  18151  tgpt0  18153  divstgphaus  18157  tsmsgsum  18173  tsmsres  18178  tsmsxplem1  18187  isust  18238  elutop  18268  utopsnneiplem  18282  utopsnnei  18284  isusp  18296  isucn  18313  isucn2  18314  ucncn  18320  ispsmet  18340  ismet  18358  isxmet  18359  metn0  18395  xmetres2  18396  elbl3ps  18426  elbl3  18427  xblpnfps  18430  xblpnf  18431  elmopn2  18480  metss  18543  stdbdxmet  18550  metcnp3  18575  metcnp  18576  metcnp2  18577  metcn  18578  txmetcnp  18582  txmetcn  18583  cfilucfil2OLD  18608  cfilucfil2  18609  blval2  18610  metuelOLD  18612  metuel  18613  metuel2  18614  metucnOLD  18623  metucn  18624  dscopn  18626  isngp3  18650  nmeq0  18669  ngppropd  18683  isnghm3  18764  isnmhm2  18791  bl2ioo  18828  metdsge  18884  metnrmlem1a  18893  addcnlem  18899  elcncf  18924  elcncf2  18925  evth  18989  elpi1  19075  nmhmcn  19133  cphipeq0  19171  ipcau2  19196  lmmbr  19216  lmmbr2  19217  iscfil2  19224  fmcfil  19230  iscau2  19235  iscau3  19236  iscau4  19237  iscauf  19238  caucfil  19241  metcld2  19264  cfilucfil4OLD  19278  cfilucfil4  19279  bcthlem1  19282  lssbn  19309  cmetcusp1OLD  19310  cmetcusp1  19311  srabn  19319  ishl2  19329  minveclem7  19341  ivth2  19357  ovolfioo  19369  ovolficc  19370  ovolshftlem1  19410  ovolicc2lem1  19418  icombl  19463  ioombl  19464  volsup2  19502  ismbf  19525  ismbfcn  19526  ismbfcn2  19534  mbfmax  19544  mbfimaopnlem  19550  mbfaddlem  19555  mbfsup  19559  mbfinf  19560  mbflimsup  19561  i1faddlem  19588  i1fres  19600  itg1ge0a  19606  itg1climres  19609  mbfi1fseqlem4  19613  itg2leub  19629  itg2const  19635  itg2split  19644  itg2cnlem2  19657  iblcnlem1  19682  iblrelem  19685  itgss3  19709  ellimc  19765  ellimc2  19769  ellimc3  19771  limcmpt  19775  limcmpt2  19776  limcres  19778  cnplimc  19779  limcun  19787  dvreslem  19801  dvcnp  19810  dvcnvlem  19865  dveflem  19868  cmvth  19880  mdegleb  19992  mdegldg  19994  degltp1le  20001  mdegle0  20005  deg1ldg  20020  coe1mul3  20027  ply1remlem  20090  fta1glem2  20094  ply1termlem  20127  coemulc  20178  coecj  20201  plymul0or  20203  ofmulrt  20204  quotval  20214  plydivlem4  20218  plyremlem  20226  ulmcau2  20317  reeff1o  20368  sincosq2sgn  20412  sinq12gt0  20420  coseq1  20435  logltb  20499  cosarg0d  20509  argrege0  20511  tanarg  20519  affineequiv  20672  dcubic1lem  20688  dcubic  20691  atandm2  20722  rlimcnp  20809  rlimcnp2  20810  xrlimcnp  20812  fsumharmonic  20855  wilthlem1  20856  ftalem7  20866  basellem3  20870  isppw2  20903  issqf  20924  sqf11  20927  mumullem2  20968  sqff1o  20970  muinv  20983  ppiublem1  20991  vmasum  21005  chpchtsum  21008  chpub  21009  dchrelbas2  21026  dchrelbas3  21027  dchrelbas4  21032  dchrinv  21050  efexple  21070  bposlem1  21073  bposlem6  21078  bposlem7  21079  lgsdilem  21111  lgsdir2lem4  21115  lgsdir2  21117  lgsne0  21122  lgsabs1  21123  lgsquad3  21150  2sqlem7  21159  2sqlem8a  21160  chtppilim  21174  dchrvmaeq0  21203  dirith  21228  ostth3  21337  isumgra  21355  wrdumgra  21356  isusgra0  21381  nbgrael  21443  nbgraeledg  21447  nb3graprlem1  21465  nb3grapr2  21468  cusgra2v  21476  cusgra3vnbpr  21479  cusgrafilem3  21495  cusgrauvtxb  21510  iswlk  21532  iswlkon  21536  trls  21541  istrl  21542  istrl2  21543  istrlon  21546  ispth  21573  isspth  21574  0spth  21576  ispthon  21581  isspthon  21588  isspthonpth  21589  1pthon  21596  wlkdvspthlem  21612  0crct  21618  0cycl  21619  fargshiftfva  21631  iseupa  21692  eupatrl  21695  eupath2lem2  21705  eupath2lem3  21706  isgrpo  21789  isablo  21876  ismgm  21913  opidon2  21917  ismndo1  21937  elghomlem2  21955  iscom2  22005  rngosn3  22019  rngosn4  22020  vci  22032  isvclem  22061  vcoprnelem  22062  nvsubadd  22141  nvelbl  22190  nvelbl2  22191  nmoubi  22278  nmobndi  22281  nmoo0  22297  isph  22328  minvecolem4b  22385  minvecolem4  22387  minvecolem5  22388  minvecolem7  22390  h2hcau  22487  h2hlm  22488  hvaddeq0  22576  hial2eq2  22614  norm-i  22636  hhssnv  22769  shsel  22821  shsel3  22822  pjhtheu2  22923  chssoc  23003  chsscon1  23008  chpsscon1  23011  chpsscon2  23012  chlejb2  23020  elspansn2  23074  fh1  23125  fh2  23126  cm2j  23127  eigposi  23344  nmopub  23416  unopf1o  23424  nmfnleub  23433  elnlfn  23436  adjvalval  23445  lnopcnre  23547  riesz4i  23571  leop2  23632  leop3  23633  leoppos  23634  hst1h  23735  mdbr2  23804  mdbr3  23805  mdbr4  23806  dmdbr2  23811  dmdbr3  23813  dmdbr4  23814  mddmd2  23817  cvdmd  23845  atcvatlem  23893  atdmd  23906  sumdmdii  23923  dmdbr5ati  23930  cdj3lem1  23942  addltmulALT  23954  raleqbid  23968  rexeqbid  23969  reuxfr3d  23981  reuxfr4d  23982  iuneq12daf  24012  csbcnvg  24042  abfmpeld  24071  abfmpel  24072  fmptdF  24074  fmptcof2  24081  disjdsct  24095  xeqlelt  24144  tltnle  24195  gsumpropd2lem  24225  isofld  24240  isinftm  24256  isarchi  24257  metidv  24292  pstmxmet  24297  lmxrge0  24342  zrhker  24366  esumlub  24457  issiga  24499  dya2ub  24625  itgeq12dv  24646  orvcgteel  24730  ballotlemfc0  24755  ballotlemfcc  24756  ballotlemrv1  24783  ballotlemrv2  24784  ballotlem1ri  24797  derangval  24858  derangenlem  24862  subfacp1lem2a  24871  subfacp1lem5  24875  erdszelem8  24889  iccllyscon  24942  cvmsval  24958  untelirr  25162  untsucf  25164  untangtr  25168  mulcan2g  25195  mulle0b  25197  mulsuble0b  25198  zprod  25268  fprodcom2  25313  dfpo2  25383  dfon2lem3  25417  dfon2lem4  25418  dfon2lem7  25421  elpredim  25456  predep  25472  preduz  25480  brbtwn  25843  brcgr  25844  eqeelen  25848  brbtwn2  25849  colinearalglem1  25850  colinearalglem2  25851  colinearalglem3  25852  colinearalg  25854  axcgrid  25860  ax5seglem4  25876  ax5seglem5  25877  axbtwnid  25883  axcontlem5  25912  axcontlem7  25914  cgrcomlr  25937  ifscgr  25983  cgr3permute2  25988  cgr3permute4  25989  cgr3permute5  25990  brcolinear2  25997  brcolinear  25998  colinearperm2  26003  colinearperm4  26004  colinearperm5  26005  brofs2  26016  brifs2  26017  btwnconn1lem3  26028  btwnconn1lem4  26029  btwnconn1lem5  26030  btwnconn1lem8  26033  btwnconn1lem10  26035  btwnconn1lem11  26036  brsegle2  26048  broutsideof3  26065  outsideofeu  26070  lineunray  26086  hfninf  26132  nndivlub  26213  wl-dedlem0a  26237  ltflcei  26247  itg2addnclem2  26271  itg2addnclem3  26272  itg2gt0cn  26274  itgaddnclem2  26278  iblabsnclem  26282  ftc1anclem1  26294  ftc1anclem5  26298  ftc1anclem7  26300  dvreasin  26304  areacirclem1  26306  areacirclem4  26309  areacirclem5  26310  areacirc  26311  elicc3  26334  nn0prpwlem  26339  nn0prpw  26340  topfneec  26385  islocfin  26390  neibastop3  26405  neifg  26414  eltail  26417  filnetlem4  26424  sdclem2  26460  fdc  26463  lmclim2  26478  0totbnd  26496  sstotbnd  26498  isbnd3b  26508  ismtyval  26523  isismty  26524  ismtyima  26526  heiborlem7  26540  heiborlem10  26543  bfplem1  26545  rrnmet  26552  rrnheibor  26560  ismrer1  26561  isdrngo2  26588  isidlc  26639  ralxpxfr2d  26755  elrfi  26762  elrfirn2  26764  isnacs2  26774  mrefg3  26776  nacsfix  26780  lzunuz  26840  diophin  26845  sbc2rexg  26858  sbc4rexg  26859  sbccomieg  26863  rexrabdioph  26868  4rexfrabdioph  26872  6rexfrabdioph  26873  diophren  26888  fiphp3d  26894  irrapxlem2  26900  elpell1qr2  26949  reglogltb  26968  reglogleb  26969  monotuz  27018  monotoddzz  27020  zindbi  27023  rmyeq0  27032  jm2.19lem2  27075  jm2.19lem3  27076  rmydioph  27099  expdiophlem1  27106  expdioph  27108  pw2f1o2val2  27125  soeq12d  27126  freq12d  27127  weeq12d  27128  fnwe2lem2  27140  islmodfg  27158  islssfg2  27160  dsmmelbas  27196  ellspd  27245  pwfi2f1o  27251  islindf  27273  islbs4  27293  islinds3  27295  islnr3  27310  rngunsnply  27369  f1omvdconj  27380  f1otrspeq  27381  pmtrmvd  27389  idomrootle  27502  caofcan  27531  pm14.122c  27615  pm14.123c  27618  sbaniota  27626  fnchoice  27690  rfcnpre3  27694  rfcnpre4  27695  climinf  27722  stoweidlem7  27746  stoweidlem27  27766  stoweidlem35  27774  sbcrel  27971  csbdmg  27972  sbcfun  27977  dfdfat2  27985  fnbrafvb  28008  afvelrnb  28017  dmfcoafv  28029  otthg  28079  sbcfn  28090  sbcf  28091  f12dfv  28098  f13dfv  28099  leaddle0  28116  2ffzeq  28144  ubmelm1fzo  28150  2ffzoeq  28163  csbwrdg  28200  wrdeq0  28204  swdeq  28230  modprm1div  28258  modprminveq  28260  cshwsiun  28320  wlkcomp  28339  usgra2pth  28349  usgra2pth0  28350  el2wlkonot  28401  el2spthonot  28402  el2spthonot0  28403  el2wlkonotot1  28406  el2wlksotot  28414  usg2wlkonot  28415  usg2wotspth  28416  2spontn0vne  28419  usg2spthonot0  28421  usg2spthonot1  28422  2spot2iun2spont  28423  nbhashuvtx1  28431  usgrauvtxvdbi  28434  isrusgra  28442  frgra3v  28466  frgrancvvdeqlem3  28495  frgrawopreglem2  28508  usg2spot2nb  28528  usgreg2spot  28530  trsbc  28699  sbcssOLD  28701  bnj984  29397  bnj1417  29484  islshpsm  29852  lrelat  29886  islshpat  29889  islshpcv  29925  ellkr  29961  lkr0f  29966  lkrsc  29969  lshpkrlem1  29982  islshpkrN  29992  lfl1dim  29993  lkrpssN  30035  ldual1dim  30038  ople0  30059  opltn0  30062  op1le  30064  opcon2b  30069  oplecon1b  30073  opltcon1b  30077  opltcon2b  30078  cmtvalN  30083  omllaw4  30118  cmt4N  30124  cmtbr3N  30126  cmtbr4N  30127  omlfh1N  30130  cvrval  30141  pats  30157  leatb  30164  atlle0  30177  atlltn0  30178  cvlatcvr1  30213  cvlatcvr2  30214  ishlat1  30224  glbconxN  30249  hlsupr2  30258  hlateq  30270  hlrelat  30273  hlrelat2  30274  cvrval5  30286  cvrexchlem  30290  atcvr0eq  30297  cvrat4  30314  3dim0  30328  3dim2  30339  2dim  30341  islln3  30381  llnexatN  30392  islpln3  30404  islpln5  30406  islvol3  30447  islvol5  30450  4atlem11  30480  4atlem12  30483  lineset  30609  psubspset  30615  ispsubsp2  30617  elpmapat  30635  pmapglbx  30640  isline3  30647  isline4N  30648  elpaddat  30675  elpadd2at  30677  pmapjoin  30723  dalawlem13  30754  ispsubcl2N  30818  lhpoc  30885  lhpmod2i2  30909  lhpmod6i1  30910  lautset  30953  pautsetN  30969  ltrnatb  31008  ltrnel  31010  ltrncnvel  31013  ltrneq  31020  trlid0b  31049  cdleme0ex2N  31095  cdleme3  31108  cdleme7  31120  cdlemefrs29bpre0  31267  cdlemg2cN  31460  cdlemg2cex  31462  cdlemk34  31781  cdlemkid3N  31804  cdlemkid4  31805  cdlemk39s  31810  cdlemk42  31812  dvhb1dimN  31857  diaord  31919  dia11N  31920  diaglbN  31927  dia1dim2  31934  dvhopellsm  31989  dibelval3  32019  dibopelval3  32020  dibeldmN  32030  dib11N  32032  dib1dim  32037  diblsmopel  32043  diclspsn  32066  dihopelvalbN  32110  dihopelvalcqat  32118  dihopelvalcpre  32120  xihopellsmN  32126  dihopellsm  32127  dihord3  32129  dihord4  32130  dih11  32137  dihglbcpreN  32172  dihmeetlem4preN  32178  dihlspsnat  32205  dihatexv2  32211  dochord2N  32243  dochord3  32244  dochkrshp2  32259  dihjatcclem4  32293  dihjat1lem  32300  dvh2dimatN  32312  lcfl2  32365  lcfl3  32366  lcfl4N  32367  lcfl7N  32373  lcfrvalsnN  32413  lcfrlem9  32422  lcdlss  32491  mapdordlem2  32509  mapd1o  32520  mapdcv  32532  mapdn0  32541  mapdindp  32543  mapdpglem3  32547  mapdpglem26  32570  mapdpglem27  32571  mapdpglem30  32574  mapdindp1  32592  lspindp5  32642  hdmap1ffval  32668  hdmap1fval  32669  hdmapffval  32701  hdmapfval  32702  hdmapeq0  32719  hdmap11  32723  hgmapffval  32760  hgmapfval  32761  hdmapoc  32806  hlhilphllem  32834
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