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  raleqbid  23131  rexeqbid  23132  reuxfr3d  23138  reuxfr4d  23139  iuneq12daf  23154  iuneq12df  23155  itgeq12dv  23196  csbcnvg  23198  xppreima  23211  abfmpeld  23218  abfmpel  23219  fmptdF  23221  fmptcof2  23229  xeqlelt  23269  cnvordtrestixx  23297  disjdsct  23369  lmxrge0  23375  lmdvg  23376  gsumpropd2lem  23379  issiga  23472  dya2ub  23575  orvcgteel  23668  derangval  23698  derangenlem  23702  subfacp1lem2a  23711  subfacp1lem5  23715  erdszelem8  23729  iccllyscon  23781  cvmsval  23797  isumgra  23867  wrdumgra  23868  iseupa  23881  eupath2lem2  23902  eupath2lem3  23903  untelirr  24054  untsucf  24056  untangtr  24060  mulcan2g  24085  mulle0b  24087  mulsuble0b  24088  dfpo2  24112  dfon2lem3  24141  dfon2lem4  24142  dfon2lem7  24145  elpredim  24176  predep  24192  preduz  24200  brbtwn  24527  brcgr  24528  eqeelen  24532  brbtwn2  24533  colinearalglem1  24534  colinearalglem2  24535  colinearalglem3  24536  colinearalg  24538  axcgrid  24544  ax5seglem4  24560  ax5seglem5  24561  axbtwnid  24567  axcontlem5  24596  axcontlem7  24598  cgrcomlr  24621  ifscgr  24667  cgr3permute2  24672  cgr3permute4  24673  cgr3permute5  24674  brcolinear2  24681  brcolinear  24682  colinearperm2  24687  colinearperm4  24688  colinearperm5  24689  brofs2  24700  brifs2  24701  btwnconn1lem3  24712  btwnconn1lem4  24713  btwnconn1lem5  24714  btwnconn1lem8  24717  btwnconn1lem10  24719  btwnconn1lem11  24720  brsegle2  24732  broutsideof3  24749  outsideofeu  24754  lineunray  24770  hfninf  24816  nndivlub  24897  wl-dedlem0a  24922  dvreasin  24923  areacirclem2  24925  areacirclem5  24929  areacirclem6  24930  areacirc  24931  neleq12d  24933  reubidvag  24935  sbcbidv2  24969  untbi12d  25022  cnvref2  25066  feq123  25068  surjsec2  25120  inttpemp  25139  repcpwti  25161  islatalg  25183  isoriso2  25213  isdir2  25292  grpodlcan  25376  vecval3b  25452  islp3  25514  istopx  25547  prcnt  25551  cnfilca  25556  flfnei2  25577  iintlem1  25610  ismgra  25710  isalg  25721  algi  25727  dualded  25783  ismona  25809  ismonc  25814  iepiclem  25823  isepic  25824  issubcata  25846  issrc  25867  isntr  25873  islimcat  25876  prismorcset  25914  cmppar3  25974  bisig0  26062  iscol2  26093  isibg2  26110  isside1  26165  isside  26166  pdiveql  26168  abhp  26173  abhp1  26174  elicc3  26228  nn0prpwlem  26238  nn0prpw  26239  topfneec  26291  islocfin  26296  neibastop3  26311  neifg  26320  eltail  26323  filnetlem4  26330  euuni2OLD  26348  sdclem2  26452  fdc  26455  lmclim2  26474  0totbnd  26497  sstotbnd  26499  isbnd3b  26509  ismtyval  26524  isismty  26525  ismtyima  26527  heiborlem7  26541  heiborlem10  26544  bfplem1  26546  rrnmet  26553  rrnheibor  26561  ismrer1  26562  isdrngo2  26589  isidlc  26640  ralxpxfr2d  26760  elrfi  26769  elrfirn2  26771  isnacs2  26781  mrefg3  26783  nacsfix  26787  lzunuz  26847  diophin  26852  sbc2rexg  26865  sbc4rexg  26866  sbccomieg  26870  rexrabdioph  26875  4rexfrabdioph  26879  6rexfrabdioph  26880  diophren  26896  fiphp3d  26902  irrapxlem2  26908  elpell1qr2  26957  reglogltb  26976  reglogleb  26977  monotuz  27026  monotoddzz  27028  zindbi  27031  rmyeq0  27040  jm2.19lem2  27083  jm2.19lem3  27084  rmydioph  27107  expdiophlem1  27114  expdioph  27116  pw2f1o2val2  27133  soeq12d  27134  freq12d  27135  weeq12d  27136  fnwe2lem2  27148  islmodfg  27167  islssfg2  27169  dsmmelbas  27205  ellspd  27254  pwfi2f1o  27260  islindf  27282  islbs4  27302  islinds3  27304  islnr3  27319  rngunsnply  27378  f1omvdconj  27389  f1otrspeq  27390  pmtrmvd  27398  idomrootle  27511  caofcan  27540  pm14.122c  27624  pm14.123c  27627  sbaniota  27635  fnchoice  27700  rfcnpre3  27704  rfcnpre4  27705  climinf  27732  stoweidlem7  27756  stoweidlem13  27762  stoweidlem27  27776  stoweidlem34  27783  stoweidlem35  27784  stoweidlem43  27792  stoweidlem59  27808  sbcrel  27979  csbdmg  27980  sbcfun  27985  dfdfat2  27994  fnbrafvb  28016  afvelrnb  28025  dmfcoafv  28036  mpt2xopoveq  28085  mpt2xopovel  28086  isusgra0  28106  nbgrael  28141  nbusgra  28143  nbgraeledg  28145  cusgra2v  28158  frgra3v  28180  trsbc  28304  sbcssOLD  28306  bnj984  28984  bnj1417  29071  islshpsm  29170  lrelat  29204  islshpat  29207  islshpcv  29243  ellkr  29279  lkr0f  29284  lkrsc  29287  lshpkrlem1  29300  islshpkrN  29310  lfl1dim  29311  lkrpssN  29353  ldual1dim  29356  ople0  29377  opltn0  29380  op1le  29382  opcon2b  29387  oplecon1b  29391  opltcon1b  29395  opltcon2b  29396  cmtvalN  29401  omllaw4  29436  cmt4N  29442  cmtbr3N  29444  cmtbr4N  29445  omlfh1N  29448  cvrval  29459  pats  29475  leatb  29482  atlle0  29495  atlltn0  29496  cvlatcvr1  29531  cvlatcvr2  29532  ishlat1  29542  glbconxN  29567  hlsupr2  29576  hlateq  29588  hlrelat  29591  hlrelat2  29592  cvrval5  29604  cvrexchlem  29608  atcvr0eq  29615  cvrat4  29632  3dim0  29646  3dim2  29657  2dim  29659  islln3  29699  llnexatN  29710  islpln3  29722  islpln5  29724  islvol3  29765  islvol5  29768  4atlem11  29798  4atlem12  29801  lineset  29927  psubspset  29933  ispsubsp2  29935  elpmapat  29953  pmapglbx  29958  isline3  29965  isline4N  29966  elpaddat  29993  elpadd2at  29995  pmapjoin  30041  dalawlem13  30072  ispsubcl2N  30136  lhpoc  30203  lhpmod2i2  30227  lhpmod6i1  30228  lautset  30271  pautsetN  30287  ltrnatb  30326  ltrnel  30328  ltrncnvel  30331  ltrneq  30338  trlid0b  30367  cdleme0ex2N  30413  cdleme3  30426  cdleme7  30438  cdlemefrs29bpre0  30585  cdlemg2cN  30778  cdlemg2cex  30780  cdlemk34  31099  cdlemkid3N  31122  cdlemkid4  31123  cdlemk39s  31128  cdlemk42  31130  dvhb1dimN  31175  diaord  31237  dia11N  31238  diaglbN  31245  dia1dim2  31252  dvhopellsm  31307  dibelval3  31337  dibopelval3  31338  dibeldmN  31348  dib11N  31350  dib1dim  31355  diblsmopel  31361  diclspsn  31384  dihopelvalbN  31428  dihopelvalcqat  31436  dihopelvalcpre  31438  xihopellsmN  31444  dihopellsm  31445  dihord3  31447  dihord4  31448  dih11  31455  dihglbcpreN  31490  dihmeetlem4preN  31496  dihlspsnat  31523  dihatexv2  31529  dochord2N  31561  dochord3  31562  dochkrshp2  31577  dihjatcclem4  31611  dihjat1lem  31618  dvh2dimatN  31630  lcfl2  31683  lcfl3  31684  lcfl4N  31685  lcfl7N  31691  lcfrvalsnN  31731  lcfrlem9  31740  lcdlss  31809  mapdordlem2  31827  mapd1o  31838  mapdcv  31850  mapdn0  31859  mapdindp  31861  mapdpglem3  31865  mapdpglem26  31888  mapdpglem27  31889  mapdpglem30  31892  mapdindp1  31910  lspindp5  31960  hdmap1ffval  31986  hdmap1fval  31987  hdmapffval  32019  hdmapfval  32020  hdmapeq0  32037  hdmap11  32041  hgmapffval  32078  hgmapfval  32079  hdmapoc  32124  hlhilphllem  32152
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