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  ax11el  2228  eleq12d  2455  neeq12d  2565  neleq12d  2645  raleqbi1dv  2855  rexeqbi1dv  2856  reueqd  2857  rmoeqd  2858  raleqbidv  2859  rexeqbidv  2860  raleqbidva  2861  rexeqbidva  2862  eueq3  3052  sbc19.21g  3168  sbcrext  3177  sbcabel  3181  sbcel1g  3213  sbceq1g  3214  sbcel2g  3215  sbceq2g  3216  sbccsb2g  3223  sbcco3g  3248  sseq12d  3320  psseq12d  3384  raaan  3678  raaanv  3679  sbcss  3681  elimhyp2v  3731  elimhyp4v  3733  keephyp2v  3737  ralsng  3789  rexsng  3790  ssunsn2  3901  2ralunsn  3946  csbunig  3965  disjeq12d  4132  disjprg  4149  breq123d  4167  sbcbr12g  4203  sbcbr1g  4204  sbcbr2g  4205  treq  4249  nalset  4281  copsex4g  4386  frirr  4500  ordtri1  4555  reusv7OLD  4675  reuxfr2d  4686  reuxfrd  4688  elpwun  4696  ordpwsuc  4735  ordunisuc2  4764  tfindsg  4780  dfom2  4787  findsg  4812  csbxpg  4845  posn  4886  frsn  4888  csbrng  5054  elrelimasn  5168  eliniseg  5173  brcodir  5193  fneq12d  5478  feq12d  5522  feq123d  5523  f1osng  5656  csbfv12g  5678  csbfv12gALT  5679  dmfco  5736  eqfnfv2  5767  fndmdifeq0  5775  fneqeql2  5778  funimass3  5785  funconstss  5787  unpreima  5795  ralrnmpt  5817  dffo3  5823  fmptco  5840  fressnfv  5859  fnsuppeq0  5892  fnunirn  5938  f1elima  5948  cocan1  5963  cocan2  5964  fliftf  5976  soisores  5986  isomin  5996  isoini  5997  f1oiso  6010  f1oweALT  6013  mpt2eq123dva  6074  ovid  6129  ov  6132  ovg  6151  caovord2d  6195  ofrfval2  6262  offveqb  6265  reldm  6337  mpt2xopoveq  6406  mpt2xopovel  6407  isprmpt2  6413  tpostpos  6435  f1ofveu  6520  oe0m1  6701  oaord1  6730  omord  6747  omlimcl  6757  oewordi  6770  oeeui  6781  nnaordr  6799  nnaordex  6817  ereq1  6848  brdifun  6868  erth2  6886  qliftfun  6925  brecop  6933  elmapg  6967  elpmg  6968  boxcutc  7041  dom2lem  7083  xpcomco  7134  pw2f1olem  7148  nndomo  7236  unfilem2  7308  domunfican  7315  indexfi  7349  elfi2  7354  supisolem  7408  hartogslem1  7444  brwdom2  7474  canthwdom  7480  infeq5i  7524  cantnfs  7554  cantnfrescl  7565  cantnfp1lem3  7569  cantnflem1b  7575  cantnflem1  7578  cnfcom3lem  7593  r1pwOLD  7705  rankxplim  7736  iscard2  7796  infxpenc2  7836  fseqenlem1  7838  fseqdom  7840  alephnbtwn  7885  alephinit  7909  iunfictbso  7928  dfac2  7944  dfac12lem2  7957  dfac12lem3  7958  kmlem2  7964  ackbij2lem2  8053  fin23lem23  8139  fin1a2lem2  8214  fin1a2lem4  8216  fin1a2lem9  8221  dcomex  8260  axdclem  8332  brdom7disj  8342  brdom6disj  8343  iundom2g  8348  axpownd  8409  fpwwe2cbv  8438  fpwwe2lem2  8440  fpwwe2lem3  8441  fpwwe2lem9  8446  fpwwe2  8451  pwfseqlem1  8466  eltskm  8651  ltapi  8713  ltmpi  8714  nlt1pi  8716  indpi  8717  nqereu  8739  ordpipq  8752  ltsonq  8779  ltanq  8781  ltrnq  8789  archnq  8790  elnpi  8798  genpass  8819  addclprlem1  8826  mulclprlem  8829  1idpr  8839  prlem934  8843  prlem936  8857  reclem4pr  8860  addgt0sr  8912  sqgt0sr  8914  ltresr  8948  leloe  9094  eqlelt  9095  negeu  9228  subadd2  9241  subcan2  9258  ltadd1  9427  leadd2  9429  ltsubadd  9430  lesubadd  9432  ltaddsub2  9435  leaddsub2  9437  ltaddpos  9450  lesub2  9455  ltnegcon1  9461  ltnegcon2  9462  lenegcon1  9464  lenegcon2  9465  addge01  9470  addge02  9471  suble0  9474  lesub0  9476  eqord2  9490  mulcan2d  9588  diveq0  9620  diveq1  9640  ltmul2  9793  lemul2  9795  ltmulgt11  9802  ltmulgt12  9803  gt0div  9808  ge0div  9809  ltmuldiv  9812  ledivmul2OLD  9820  ltdiv2  9827  ltrec1  9829  lerec2  9830  ledivdiv  9831  ltdiv23  9833  lediv23  9834  creur  9926  creui  9927  ofsubeq0  9929  nn1suc  9953  nnrecl  10151  nn0sub  10202  znnsub  10254  btwnnz  10278  gtndiv  10279  uzindOLD  10296  eluz2  10426  uzwo  10471  uzwoOLD  10472  indstr2  10486  negn0  10494  rpneg  10573  xrleloe  10669  xltadd2  10768  xsubge0  10772  xlesubadd  10774  xmulasslem  10796  xlemul2  10802  xltmul2  10804  supxrre2  10842  elixx3g  10861  ioo0  10873  iccid  10893  ico0  10894  ioc0  10895  icc0  10896  elioc2  10905  elico2  10906  elicc2  10907  elfz2  10982  fzen  11004  fzsubel  11020  fzpr  11033  fzrevral2  11062  fzrevral3  11063  fzshftral  11064  fzosplitsni  11123  btwnzge0  11157  mod0  11182  negmod0  11183  nn0ennn  11245  expeq0  11337  sq11  11381  sq01  11428  hashen  11558  hashnncl  11572  hashsdom  11582  seqcoll2  11640  ccatopth2  11704  cnpart  11972  sqrlem7  11981  sqrneglem  11999  sqabs  12039  abslt  12045  absle  12046  absdiflt  12048  absdifle  12049  lenegsq  12051  rexanuz2  12080  limsupgle  12198  limsuple  12199  clim  12215  rlim  12216  clim0c  12228  rlim0  12229  rlim0lt  12230  ello12  12237  ello1mpt  12242  elo12  12248  lo1o12  12254  elo1mpt  12255  elo1mpt2  12256  o1lo1  12258  isercolllem2  12386  isercoll2  12389  zsum  12439  fsum2dlem  12481  fsumcom2  12485  binomlem  12535  efieq  12691  sin01bnd  12713  cos01bnd  12714  dvdsval2  12782  dvdsaddr  12816  fzocongeq  12830  odd2np1  12835  divalglem4  12843  divalglem5  12844  divalgb  12851  bits0  12867  bitsp1e  12871  bitsp1o  12872  bitscmp  12877  bitsinv1lem  12880  sadval  12895  sadcaddlem  12896  smuval  12920  smuval2  12921  dvdssq  12987  nn0seqcvgd  12988  algcvgblem  12995  isprm2  13014  qredeq  13033  prmdvdsexp  13041  prmdvdsexpb  13042  prmexpb  13044  prmfac1  13045  qnumgt0  13069  hashdvds  13091  fermltl  13100  pcpremul  13144  pc2dvds  13179  pcz  13181  prmpwdvds  13199  prmreclem5  13215  4sqlem16  13255  vdwapun  13269  vdwmc  13273  vdwlem6  13281  ramval  13303  prdsbasmpt  13619  prdsleval  13626  prdsbasmpt2  13631  imasleval  13693  xpsle  13733  mrcidb2  13770  ismri  13783  mrieqvd  13790  acsfiel  13806  acsfn2  13815  catpropd  13862  ismon2  13887  isepi2  13894  isinv  13912  isssc  13947  subsubc  13977  funcres2b  14021  funcpropd  14024  isfull  14034  isfth  14038  fullpropd  14044  isnat2  14072  fucsect  14096  fuciso  14099  elsetchom  14163  setcsect  14171  setciso  14173  isprs  14314  isdrs  14318  posi  14334  pltval3  14351  istos  14391  islat  14403  latleeqj1  14419  latleeqj2  14420  latleeqm1  14435  latleeqm2  14436  ipodrsima  14518  isacs5  14525  acsficl2d  14529  isdlat  14546  mhmpropd  14671  issubm2  14676  gsumvalx  14701  gsumpropd  14703  grpsubrcan  14797  grplactcnv  14814  issubg  14871  eqgval  14916  conjnmzb  14967  isga  14995  odmulg  15119  odf1o1  15133  odngen  15138  gexdvds  15145  pgpfi2  15167  isslw  15169  slwpss  15173  pgpssslw  15175  subgslw  15177  sylow2alem2  15179  fislw  15186  sylow3lem2  15189  lsmelvalm  15212  lsmdisj3a  15248  pj1eq  15259  iscmn  15346  eqgabl  15381  torsubg  15396  gsumval3  15441  dprdf11  15508  dprd2da  15527  dmdprdpr  15534  ablfac1eulem  15557  pgpfac1lem2  15560  pgpfac1lem3a  15561  pgpfac1lem3  15562  rngpropd  15622  dvdsrval  15677  dvdsr02  15688  unitpropd  15729  drngmuleq0  15785  drngpropd  15789  issubrg  15795  islmod  15881  lsmelpr  16090  lspsnne1  16116  fidomndrnglem  16293  coe1mul2lem2  16588  coe1tm  16592  prmirredlem  16696  prmirred  16698  domnchr  16736  znleval  16758  znchr  16766  znunithash  16768  iscss2  16836  ishil2  16869  istopg  16891  eltg  16945  eltg2  16946  tgss2  16975  bastop1  16981  bastop2  16982  iscld  17014  iscld4  17052  elcls2  17061  elcls3  17070  isclo  17074  mretopd  17079  isnei  17090  neiint  17091  neindisj2  17110  islp2  17132  maxlp  17133  cldlp  17136  neitr  17166  iscn  17221  iscnp  17223  iscnp3  17230  tgcn  17238  subbascn  17240  ssidcn  17241  lmbr2  17245  lmbrf  17246  cnnei  17268  cnrest2  17272  hausnei2  17339  cmpsub  17385  tgcmp  17386  cmpfi  17393  consuba  17404  connsub  17405  dis2ndc  17444  subislly  17465  elkgen  17489  kgencn  17509  kgencn2  17510  eltx  17521  ptpjpre1  17524  ptcnplem  17574  hausdiag  17598  xkoptsub  17607  xkoco2cn  17611  imasnopn  17643  imasncld  17644  imasncls  17645  elqtop  17650  qtopcld  17666  kqcldsat  17686  kqt0lem  17689  isr0  17690  regr1lem2  17693  ordthmeolem  17754  ptuncnv  17760  trfbas  17797  elfg  17824  trfil3  17841  trufil  17863  filufint  17873  uffix2  17877  elfm2  17901  elfm3  17903  flimtopon  17923  flimopn  17928  fbflim  17929  fbflim2  17930  flffbas  17948  flftg  17949  cnflf  17955  txflf  17959  isfcls  17962  fclstopon  17965  fclsbas  17974  fclsrest  17977  fcfnei  17988  cnfcf  17995  ptcmplem2  18005  tgphaus  18067  tgpt0  18069  divstgphaus  18073  tsmsgsum  18089  tsmsres  18094  tsmsxplem1  18103  isust  18154  elutop  18184  utopsnneiplem  18198  utopsnnei  18200  isusp  18212  isucn  18229  isucn2  18230  ucncn  18236  ismet  18262  isxmet  18263  metn0  18298  xmetres2  18299  elbl3  18325  xblpnf  18327  elmopn2  18365  metss  18428  stdbdxmet  18435  metcnp3  18460  metcnp  18461  metcnp2  18462  metcn  18463  txmetcnp  18467  txmetcn  18468  cfilucfil2  18481  blval2  18482  metuel  18484  metuel2  18485  metucn  18490  dscopn  18492  isngp3  18516  nmeq0  18535  ngppropd  18549  isnghm3  18630  isnmhm2  18657  bl2ioo  18694  metdsge  18750  metnrmlem1a  18759  addcnlem  18765  elcncf  18790  elcncf2  18791  evth  18855  elpi1  18941  nmhmcn  18999  cphipeq0  19037  ipcau2  19062  lmmbr  19082  lmmbr2  19083  iscfil2  19090  fmcfil  19096  iscau2  19101  iscau3  19102  iscau4  19103  iscauf  19104  caucfil  19107  metcld2  19130  cfilucfil4  19143  bcthlem1  19146  lssbn  19173  cmetcusp1  19174  srabn  19181  ishl2  19191  minveclem7  19203  ivth2  19219  ovolfioo  19231  ovolficc  19232  ovolshftlem1  19272  ovolicc2lem1  19280  icombl  19325  ioombl  19326  volsup2  19364  ismbf  19389  ismbfcn  19390  ismbfcn2  19398  mbfmax  19408  mbfimaopnlem  19414  mbfaddlem  19419  mbfsup  19423  mbfinf  19424  mbflimsup  19425  i1faddlem  19452  i1fres  19464  itg1ge0a  19470  itg1climres  19473  mbfi1fseqlem4  19477  itg2leub  19493  itg2const  19499  itg2split  19508  itg2cnlem2  19521  iblcnlem1  19546  iblrelem  19549  itgss3  19573  ellimc  19627  ellimc2  19631  ellimc3  19633  limcmpt  19637  limcmpt2  19638  limcres  19640  cnplimc  19641  limcun  19649  dvreslem  19663  dvcnp  19672  dvcnvlem  19727  dveflem  19730  cmvth  19742  mdegleb  19854  mdegldg  19856  degltp1le  19863  mdegle0  19867  deg1ldg  19882  coe1mul3  19889  ply1remlem  19952  fta1glem2  19956  ply1termlem  19989  coemulc  20040  coecj  20063  plymul0or  20065  ofmulrt  20066  quotval  20076  plydivlem4  20080  plyremlem  20088  ulmcau2  20179  reeff1o  20230  sincosq2sgn  20274  sinq12gt0  20282  coseq1  20297  logltb  20361  cosarg0d  20371  argrege0  20373  tanarg  20381  affineequiv  20534  dcubic1lem  20550  dcubic  20553  atandm2  20584  rlimcnp  20671  rlimcnp2  20672  xrlimcnp  20674  fsumharmonic  20717  wilthlem1  20718  ftalem7  20728  basellem3  20732  isppw2  20765  issqf  20786  sqf11  20789  mumullem2  20830  sqff1o  20832  muinv  20845  ppiublem1  20853  vmasum  20867  chpchtsum  20870  chpub  20871  dchrelbas2  20888  dchrelbas3  20889  dchrelbas4  20894  dchrinv  20912  efexple  20932  bposlem1  20935  bposlem6  20940  bposlem7  20941  lgsdilem  20973  lgsdir2lem4  20977  lgsdir2  20979  lgsne0  20984  lgsabs1  20985  lgsquad3  21012  2sqlem7  21021  2sqlem8a  21022  chtppilim  21036  dchrvmaeq0  21065  dirith  21090  ostth3  21199  isumgra  21217  wrdumgra  21218  isusgra0  21243  nbgrael  21304  nbusgra  21306  nbgraeledg  21308  nb3graprlem1  21326  nb3grapr2  21329  cusgra2v  21337  cusgra3vnbpr  21340  cusgrafilem3  21356  cusgrauvtxb  21371  iswlk  21391  iswlkon  21395  trls  21400  istrl  21401  istrl2  21402  istrlon  21405  ispth  21422  isspth  21423  0spth  21425  ispthon  21430  1pthon  21439  wlkdvspthlem  21455  0crct  21461  0cycl  21462  fargshiftfva  21474  iseupa  21535  eupatrl  21538  eupath2lem2  21548  eupath2lem3  21549  isgrpo  21632  isablo  21719  ismgm  21756  opidon2  21760  ismndo1  21780  elghomlem2  21798  iscom2  21848  rngosn3  21862  rngosn4  21863  vci  21875  isvclem  21904  vcoprnelem  21905  nvsubadd  21984  nvelbl  22033  nvelbl2  22034  nmoubi  22121  nmobndi  22124  nmoo0  22140  isph  22171  minvecolem4b  22228  minvecolem4  22230  minvecolem5  22231  minvecolem7  22233  h2hcau  22330  h2hlm  22331  hvaddeq0  22419  hial2eq2  22457  norm-i  22479  hhssnv  22612  shsel  22664  shsel3  22665  pjhtheu2  22766  chssoc  22846  chsscon1  22851  chpsscon1  22854  chpsscon2  22855  chlejb2  22863  elspansn2  22917  fh1  22968  fh2  22969  cm2j  22970  eigposi  23187  nmopub  23259  unopf1o  23267  nmfnleub  23276  elnlfn  23279  adjvalval  23288  lnopcnre  23390  riesz4i  23414  leop2  23475  leop3  23476  leoppos  23477  hst1h  23578  mdbr2  23647  mdbr3  23648  mdbr4  23649  dmdbr2  23654  dmdbr3  23656  dmdbr4  23657  mddmd2  23660  cvdmd  23688  atcvatlem  23736  atdmd  23749  sumdmdii  23766  dmdbr5ati  23773  cdj3lem1  23785  addltmulALT  23797  raleqbid  23807  rexeqbid  23808  reuxfr3d  23820  reuxfr4d  23821  iuneq12daf  23851  csbcnvg  23880  abfmpeld  23908  abfmpel  23909  fmptdF  23911  fmptcof2  23918  disjdsct  23931  xeqlelt  23975  gsumpropd2lem  24049  isofld  24061  lmxrge0  24141  zrhker  24160  esumlub  24248  issiga  24290  dya2ub  24414  itgeq12dv  24435  orvcgteel  24504  ballotlemfc0  24529  ballotlemfcc  24530  ballotlemrv1  24557  ballotlemrv2  24558  ballotlem1ri  24571  derangval  24632  derangenlem  24636  subfacp1lem2a  24645  subfacp1lem5  24649  erdszelem8  24663  iccllyscon  24716  cvmsval  24732  untelirr  24936  untsucf  24938  untangtr  24942  mulcan2g  24969  mulle0b  24971  mulsuble0b  24972  zprod  25042  dfpo2  25136  dfon2lem3  25165  dfon2lem4  25166  dfon2lem7  25169  elpredim  25200  predep  25216  preduz  25224  brbtwn  25552  brcgr  25553  eqeelen  25557  brbtwn2  25558  colinearalglem1  25559  colinearalglem2  25560  colinearalglem3  25561  colinearalg  25563  axcgrid  25569  ax5seglem4  25585  ax5seglem5  25586  axbtwnid  25592  axcontlem5  25621  axcontlem7  25623  cgrcomlr  25646  ifscgr  25692  cgr3permute2  25697  cgr3permute4  25698  cgr3permute5  25699  brcolinear2  25706  brcolinear  25707  colinearperm2  25712  colinearperm4  25713  colinearperm5  25714  brofs2  25725  brifs2  25726  btwnconn1lem3  25737  btwnconn1lem4  25738  btwnconn1lem5  25739  btwnconn1lem8  25742  btwnconn1lem10  25744  btwnconn1lem11  25745  brsegle2  25757  broutsideof3  25774  outsideofeu  25779  lineunray  25795  hfninf  25841  nndivlub  25922  wl-dedlem0a  25946  ltflcei  25950  itg2addnclem  25957  itg2addnclem2  25958  itg2addnc  25959  itg2gt0cn  25960  itgaddnclem2  25964  iblabsnclem  25968  dvreasin  25980  areacirclem2  25982  areacirclem5  25986  areacirclem6  25987  areacirc  25988  elicc3  26011  nn0prpwlem  26016  nn0prpw  26017  topfneec  26062  islocfin  26067  neibastop3  26082  neifg  26091  eltail  26094  filnetlem4  26101  sdclem2  26137  fdc  26140  lmclim2  26155  0totbnd  26173  sstotbnd  26175  isbnd3b  26185  ismtyval  26200  isismty  26201  ismtyima  26203  heiborlem7  26217  heiborlem10  26220  bfplem1  26222  rrnmet  26229  rrnheibor  26237  ismrer1  26238  isdrngo2  26265  isidlc  26316  ralxpxfr2d  26432  elrfi  26439  elrfirn2  26441  isnacs2  26451  mrefg3  26453  nacsfix  26457  lzunuz  26517  diophin  26522  sbc2rexg  26535  sbc4rexg  26536  sbccomieg  26540  rexrabdioph  26545  4rexfrabdioph  26549  6rexfrabdioph  26550  diophren  26565  fiphp3d  26571  irrapxlem2  26577  elpell1qr2  26626  reglogltb  26645  reglogleb  26646  monotuz  26695  monotoddzz  26697  zindbi  26700  rmyeq0  26709  jm2.19lem2  26752  jm2.19lem3  26753  rmydioph  26776  expdiophlem1  26783  expdioph  26785  pw2f1o2val2  26802  soeq12d  26803  freq12d  26804  weeq12d  26805  fnwe2lem2  26817  islmodfg  26836  islssfg2  26838  dsmmelbas  26874  ellspd  26923  pwfi2f1o  26929  islindf  26951  islbs4  26971  islinds3  26973  islnr3  26988  rngunsnply  27047  f1omvdconj  27058  f1otrspeq  27059  pmtrmvd  27067  idomrootle  27180  caofcan  27209  pm14.122c  27293  pm14.123c  27296  sbaniota  27304  fnchoice  27368  rfcnpre3  27372  rfcnpre4  27373  climinf  27400  stoweidlem7  27424  stoweidlem27  27444  stoweidlem35  27452  sbcrel  27649  csbdmg  27650  sbcfun  27655  dfdfat2  27664  fnbrafvb  27687  afvelrnb  27696  dmfcoafv  27708  frgra3v  27755  frgrancvvdeqlem3  27784  frgrawopreglem2  27797  trsbc  27968  sbcssOLD  27970  bnj984  28661  bnj1417  28748  islshpsm  29095  lrelat  29129  islshpat  29132  islshpcv  29168  ellkr  29204  lkr0f  29209  lkrsc  29212  lshpkrlem1  29225  islshpkrN  29235  lfl1dim  29236  lkrpssN  29278  ldual1dim  29281  ople0  29302  opltn0  29305  op1le  29307  opcon2b  29312  oplecon1b  29316  opltcon1b  29320  opltcon2b  29321  cmtvalN  29326  omllaw4  29361  cmt4N  29367  cmtbr3N  29369  cmtbr4N  29370  omlfh1N  29373  cvrval  29384  pats  29400  leatb  29407  atlle0  29420  atlltn0  29421  cvlatcvr1  29456  cvlatcvr2  29457  ishlat1  29467  glbconxN  29492  hlsupr2  29501  hlateq  29513  hlrelat  29516  hlrelat2  29517  cvrval5  29529  cvrexchlem  29533  atcvr0eq  29540  cvrat4  29557  3dim0  29571  3dim2  29582  2dim  29584  islln3  29624  llnexatN  29635  islpln3  29647  islpln5  29649  islvol3  29690  islvol5  29693  4atlem11  29723  4atlem12  29726  lineset  29852  psubspset  29858  ispsubsp2  29860  elpmapat  29878  pmapglbx  29883  isline3  29890  isline4N  29891  elpaddat  29918  elpadd2at  29920  pmapjoin  29966  dalawlem13  29997  ispsubcl2N  30061  lhpoc  30128  lhpmod2i2  30152  lhpmod6i1  30153  lautset  30196  pautsetN  30212  ltrnatb  30251  ltrnel  30253  ltrncnvel  30256  ltrneq  30263  trlid0b  30292  cdleme0ex2N  30338  cdleme3  30351  cdleme7  30363  cdlemefrs29bpre0  30510  cdlemg2cN  30703  cdlemg2cex  30705  cdlemk34  31024  cdlemkid3N  31047  cdlemkid4  31048  cdlemk39s  31053  cdlemk42  31055  dvhb1dimN  31100  diaord  31162  dia11N  31163  diaglbN  31170  dia1dim2  31177  dvhopellsm  31232  dibelval3  31262  dibopelval3  31263  dibeldmN  31273  dib11N  31275  dib1dim  31280  diblsmopel  31286  diclspsn  31309  dihopelvalbN  31353  dihopelvalcqat  31361  dihopelvalcpre  31363  xihopellsmN  31369  dihopellsm  31370  dihord3  31372  dihord4  31373  dih11  31380  dihglbcpreN  31415  dihmeetlem4preN  31421  dihlspsnat  31448  dihatexv2  31454  dochord2N  31486  dochord3  31487  dochkrshp2  31502  dihjatcclem4  31536  dihjat1lem  31543  dvh2dimatN  31555  lcfl2  31608  lcfl3  31609  lcfl4N  31610  lcfl7N  31616  lcfrvalsnN  31656  lcfrlem9  31665  lcdlss  31734  mapdordlem2  31752  mapd1o  31763  mapdcv  31775  mapdn0  31784  mapdindp  31786  mapdpglem3  31790  mapdpglem26  31813  mapdpglem27  31814  mapdpglem30  31817  mapdindp1  31835  lspindp5  31885  hdmap1ffval  31911  hdmap1fval  31912  hdmapffval  31944  hdmapfval  31945  hdmapeq0  31962  hdmap11  31966  hgmapffval  32003  hgmapfval  32004  hdmapoc  32049  hlhilphllem  32077
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