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  2146  eleq12d  2364  neeq12d  2474  raleqbi1dv  2757  rexeqbi1dv  2758  reueqd  2759  rmoeqd  2760  raleqbidv  2761  rexeqbidv  2762  raleqbidva  2763  rexeqbidva  2764  eueq3  2953  sbc19.21g  3068  sbcrext  3077  sbcabel  3081  sbcel1g  3113  sbceq1g  3114  sbcel2g  3115  sbceq2g  3116  sbccsb2g  3123  sbcco3g  3149  sseq12d  3220  psseq12d  3283  raaan  3574  raaanv  3575  sbcss  3577  elimhyp2v  3627  elimhyp4v  3629  keephyp2v  3633  ralsng  3685  rexsng  3686  ssunsn2  3789  2ralunsn  3832  csbunig  3851  disjeq12d  4018  disjprg  4035  breq123d  4053  sbcbr12g  4089  sbcbr1g  4090  sbcbr2g  4091  treq  4135  nalset  4167  copsex4g  4271  frirr  4386  ordtri1  4441  reusv7OLD  4562  reuxfr2d  4573  reuxfrd  4575  elpwun  4583  ordpwsuc  4622  ordunisuc2  4651  tfindsg  4667  dfom2  4674  findsg  4699  csbxpg  4732  posn  4774  frsn  4776  csbrng  4939  elrelimasn  5053  eliniseg  5058  brcodir  5078  fneq12d  5353  feq12d  5397  feq123d  5398  f1osng  5530  f1oprswap  5531  csbfv12g  5551  csbfv12gALT  5552  dmfco  5609  eqfnfv2  5639  fndmdifeq0  5647  fneqeql2  5650  funimass3  5657  funconstss  5659  unpreima  5667  ralrnmpt  5685  dffo3  5691  fmptco  5707  fressnfv  5723  fnsuppeq0  5749  fnunirn  5794  f1elima  5803  cocan1  5817  cocan2  5818  fliftf  5830  soisores  5840  isomin  5850  isoini  5851  f1oiso  5864  f1oweALT  5867  mpt2eq123dva  5925  ovid  5980  ov  5983  ovg  6002  caovord2d  6045  ofrfval2  6112  offveqb  6115  reldm  6187  tpostpos  6270  f1ofveu  6355  oe0m1  6536  oaord1  6565  omord  6582  omlimcl  6592  oewordi  6605  oeeui  6616  nnaordr  6634  nnaordex  6652  ereq1  6683  brdifun  6703  erth2  6721  qliftfun  6759  brecop  6767  elmapg  6801  elpmg  6802  boxcutc  6875  dom2lem  6917  xpcomco  6968  pw2f1olem  6982  nndomo  7070  unfilem2  7138  domunfican  7145  indexfi  7179  elfi2  7184  supisolem  7237  hartogslem1  7273  brwdom2  7303  canthwdom  7309  infeq5i  7353  cantnfs  7383  cantnfrescl  7394  cantnfp1lem3  7398  cantnflem1b  7404  cantnflem1  7407  cnfcom3lem  7422  r1pwOLD  7534  rankxplim  7565  iscard2  7625  infxpenc2  7665  fseqenlem1  7667  fseqdom  7669  alephnbtwn  7714  alephinit  7738  iunfictbso  7757  dfac2  7773  dfac12lem2  7786  dfac12lem3  7787  kmlem2  7793  ackbij2lem2  7882  fin23lem23  7968  fin1a2lem2  8043  fin1a2lem4  8045  fin1a2lem9  8050  dcomex  8089  axdclem  8162  brdom7disj  8172  brdom6disj  8173  iundom2g  8178  axpownd  8239  fpwwe2cbv  8268  fpwwe2lem2  8270  fpwwe2lem3  8271  fpwwe2lem9  8276  fpwwe2  8281  pwfseqlem1  8296  eltskm  8481  ltapi  8543  ltmpi  8544  nlt1pi  8546  indpi  8547  nqereu  8569  ordpipq  8582  ltsonq  8609  ltanq  8611  ltrnq  8619  archnq  8620  elnpi  8628  genpass  8649  addclprlem1  8656  mulclprlem  8659  1idpr  8669  prlem934  8673  prlem936  8687  reclem4pr  8690  addgt0sr  8742  sqgt0sr  8744  ltresr  8778  leloe  8924  eqlelt  8925  negeu  9058  subadd2  9071  subcan2  9088  ltadd1  9257  leadd2  9259  ltsubadd  9260  lesubadd  9262  ltaddsub2  9265  leaddsub2  9267  ltaddpos  9280  lesub2  9285  ltnegcon1  9291  ltnegcon2  9292  lenegcon1  9294  lenegcon2  9295  addge01  9300  addge02  9301  suble0  9304  lesub0  9306  eqord2  9320  mulcan2d  9418  diveq0  9450  diveq1  9470  ltmul2  9623  lemul2  9625  ltmulgt11  9632  ltmulgt12  9633  gt0div  9638  ge0div  9639  ltmuldiv  9642  ledivmul2OLD  9650  ltdiv2  9657  ltrec1  9659  lerec2  9660  ledivdiv  9661  ltdiv23  9663  lediv23  9664  creur  9756  creui  9757  ofsubeq0  9759  nn1suc  9783  nnrecl  9979  nn0sub  10030  znnsub  10080  btwnnz  10104  gtndiv  10105  uzindOLD  10122  eluz2  10252  uzwo  10297  uzwoOLD  10298  indstr2  10312  negn0  10320  rpneg  10399  xrleloe  10494  xltadd2  10593  xsubge0  10597  xlesubadd  10599  xmulasslem  10621  xlemul2  10627  xltmul2  10629  supxrre2  10666  elixx3g  10685  ioo0  10697  iccid  10717  ico0  10718  ioc0  10719  icc0  10720  elioc2  10729  elico2  10730  elicc2  10731  elfz2  10805  fzen  10827  fzsubel  10843  fzpr  10856  fzrevral2  10883  fzrevral3  10884  fzshftral  10885  fzosplitsni  10937  btwnzge0  10969  mod0  10994  negmod0  10995  nn0ennn  11057  expeq0  11148  sq11  11192  sq01  11239  hashen  11362  hashnncl  11370  hashsdom  11379  seqcoll2  11418  ccatopth2  11479  cnpart  11741  sqrlem7  11750  sqrneglem  11768  sqabs  11808  abslt  11814  absle  11815  absdiflt  11817  absdifle  11818  lenegsq  11820  rexanuz2  11849  limsupgle  11967  limsuple  11968  clim  11984  rlim  11985  clim0c  11997  rlim0  11998  rlim0lt  11999  ello12  12006  ello1mpt  12011  elo12  12017  lo1o12  12023  elo1mpt  12024  elo1mpt2  12025  o1lo1  12027  isercolllem2  12155  isercoll2  12158  zsum  12207  fsum2dlem  12249  fsumcom2  12253  binomlem  12303  efieq  12459  sin01bnd  12481  cos01bnd  12482  dvdsval2  12550  dvdsaddr  12584  fzocongeq  12598  odd2np1  12603  divalglem4  12611  divalglem5  12612  divalgb  12619  bits0  12635  bitsp1e  12639  bitsp1o  12640  bitscmp  12645  bitsinv1lem  12648  sadval  12663  sadcaddlem  12664  smuval  12688  smuval2  12689  dvdssq  12755  nn0seqcvgd  12756  algcvgblem  12763  isprm2  12782  qredeq  12801  prmdvdsexp  12809  prmdvdsexpb  12810  prmexpb  12812  prmfac1  12813  qnumgt0  12837  hashdvds  12859  fermltl  12868  pcpremul  12912  pc2dvds  12947  pcz  12949  prmpwdvds  12967  prmreclem5  12983  4sqlem16  13023  vdwapun  13037  vdwmc  13041  vdwlem6  13049  ramval  13071  prdsbasmpt  13385  prdsleval  13392  prdsbasmpt2  13397  imasleval  13459  xpsle  13499  mrcidb2  13536  ismri  13549  mrieqvd  13556  acsfiel  13572  acsfn2  13581  catpropd  13628  cidpropd  13629  ismon2  13653  isepi2  13660  isinv  13678  isssc  13713  subsubc  13743  funcres2b  13787  funcpropd  13790  isfull  13800  isfth  13804  fullpropd  13810  isnat2  13838  fucsect  13862  fuciso  13865  elsetchom  13929  setcsect  13937  setciso  13939  evlfcl  14012  isprs  14080  isdrs  14084  posi  14100  pltval3  14117  istos  14157  islat  14169  latleeqj1  14185  latleeqj2  14186  latleeqm1  14201  latleeqm2  14202  ipodrsima  14284  isacs5  14291  acsficl2d  14295  isdlat  14312  ismgmid  14403  mhmpropd  14437  issubm2  14442  gsumvalx  14467  gsumpropd  14469  grpsubrcan  14563  grplactcnv  14580  issubg  14637  eqgval  14682  conjnmzb  14733  isga  14761  odmulg  14885  odf1o1  14899  odngen  14904  gexdvds  14911  pgpfi2  14933  isslw  14935  slwpss  14939  pgpssslw  14941  subgslw  14943  sylow2alem2  14945  fislw  14952  sylow3lem2  14955  lsmelvalm  14978  lsmdisj3a  15014  pj1eq  15025  iscmn  15112  eqgabl  15147  torsubg  15162  gsumval3  15207  dprdf11  15274  dprd2da  15293  dmdprdpr  15300  ablfac1eulem  15323  pgpfac1lem2  15326  pgpfac1lem3a  15327  pgpfac1lem3  15328  rngpropd  15388  dvdsrval  15443  dvdsr02  15454  unitpropd  15495  drngmuleq0  15551  drngpropd  15555  issubrg  15561  islmod  15647  lsmelpr  15860  lspsnne1  15886  fidomndrnglem  16063  coe1mul2lem2  16361  coe1tm  16365  prmirredlem  16462  prmirred  16464  domnchr  16502  znleval  16524  znchr  16532  znunithash  16534  iscss2  16602  ishil2  16635  istopg  16657  eltg  16711  eltg2  16712  tgss2  16741  bastop1  16747  bastop2  16748  iscld  16780  iscld4  16818  elcls2  16827  elcls3  16836  isclo  16840  mretopd  16845  isnei  16856  neiint  16857  neindisj2  16876  islp2  16893  maxlp  16894  cldlp  16897  iscn  16981  iscnp  16983  iscnp3  16990  tgcn  16998  subbascn  17000  ssidcn  17001  lmbr2  17005  lmbrf  17006  cnrest2  17030  hausnei2  17097  cmpsub  17143  tgcmp  17144  cmpfi  17151  consuba  17162  connsub  17163  dis2ndc  17202  subislly  17223  elkgen  17247  kgencn  17267  kgencn2  17268  eltx  17279  ptpjpre1  17282  ptcnplem  17331  hausdiag  17355  xkoptsub  17364  xkoco2cn  17368  elqtop  17404  qtopcld  17420  kqcldsat  17440  kqt0lem  17443  isr0  17444  regr1lem2  17447  ordthmeolem  17508  ptuncnv  17514  trfbas  17555  elfg  17582  trfil3  17599  trufil  17621  filufint  17631  uffix2  17635  elfm2  17659  elfm3  17661  flimtopon  17681  flimopn  17686  fbflim  17687  fbflim2  17688  flffbas  17706  flftg  17707  cnflf  17713  txflf  17717  isfcls  17720  fclstopon  17723  fclsbas  17732  fclsrest  17735  fcfnei  17746  cnfcf  17753  ptcmplem2  17763  tgphaus  17815  tgpt0  17817  divstgphaus  17821  tsmsgsum  17837  tsmsres  17842  tsmsxplem1  17851  ismet  17904  isxmet  17905  metn0  17940  xmetres2  17941  elbl3  17967  xblpnf  17969  elmopn2  18007  metss  18070  stdbdxmet  18077  metcnp3  18102  metcnp  18103  metcnp2  18104  metcn  18105  txmetcnp  18109  txmetcn  18110  dscopn  18112  isngp3  18136  nmeq0  18155  ngppropd  18169  isnghm3  18250  isnmhm2  18277  bl2ioo  18314  metdsge  18369  metnrmlem1a  18378  addcnlem  18384  elcncf  18409  elcncf2  18410  evth  18473  elpi1  18559  nmhmcn  18617  cphipeq0  18655  ipcau2  18680  lmmbr  18700  lmmbr2  18701  iscfil2  18708  fmcfil  18714  iscau  18718  iscau2  18719  iscau3  18720  iscau4  18721  iscauf  18722  caucfil  18725  metcld2  18748  bcthlem1  18762  lssbn  18789  srabn  18793  ishl2  18803  minveclem7  18815  ivth2  18831  ovolfioo  18843  ovolficc  18844  ovolshftlem1  18884  ovolicc2lem1  18892  icombl  18937  ioombl  18938  volsup2  18976  ismbf  19001  ismbfcn  19002  ismbfcn2  19010  mbfmax  19020  mbfimaopnlem  19026  mbfaddlem  19031  mbfsup  19035  mbfinf  19036  mbflimsup  19037  i1faddlem  19064  i1fres  19076  itg1ge0a  19082  itg1climres  19085  mbfi1fseqlem4  19089  itg2leub  19105  itg2const  19111  itg2split  19120  itg2cnlem2  19133  iblcnlem1  19158  iblrelem  19161  itgss3  19185  ellimc  19239  ellimc2  19243  ellimc3  19245  limcmpt  19249  limcmpt2  19250  limcres  19252  cnplimc  19253  limcun  19261  dvreslem  19275  dvcnp  19284  dvcnvlem  19339  dveflem  19342  cmvth  19354  mdegleb  19466  mdegldg  19468  degltp1le  19475  mdegle0  19479  deg1ldg  19494  coe1mul3  19501  ply1remlem  19564  fta1glem2  19568  ply1termlem  19601  coemulc  19652  coecj  19675  plymul0or  19677  ofmulrt  19678  quotval  19688  plydivlem4  19692  plyremlem  19700  ulmcau2  19789  reeff1o  19839  sincosq2sgn  19883  sinq12gt0  19891  coseq1  19906  logltb  19969  cosarg0d  19979  argrege0  19981  tanarg  19986  affineequiv  20139  dcubic1lem  20155  dcubic  20158  atandm2  20189  rlimcnp  20276  rlimcnp2  20277  xrlimcnp  20279  fsumharmonic  20321  wilthlem1  20322  ftalem7  20332  basellem3  20336  isppw2  20369  issqf  20390  sqf11  20393  mumullem2  20434  sqff1o  20436  muinv  20449  ppiublem1  20457  vmasum  20471  chpchtsum  20474  chpub  20475  dchrelbas2  20492  dchrelbas3  20493  dchrelbas4  20498  dchrinv  20516  efexple  20536  bposlem1  20539  bposlem6  20544  bposlem7  20545  lgsdilem  20577  lgsdir2lem4  20581  lgsdir2  20583  lgsne0  20588  lgsabs1  20589  lgsquad3  20616  2sqlem7  20625  2sqlem8a  20626  chtppilim  20640  dchrvmaeq0  20669  dirith  20694  ostth3  20803  isgrpo  20879  isablo  20966  ismgm  21003  opidon2  21007  ismndo1  21027  elghomlem2  21045  isrngo  21061  iscom2  21095  rngosn3  21109  rngosn4  21110  vci  21120  isvclem  21149  vcoprnelem  21150  nvsubadd  21229  nvelbl  21278  nvelbl2  21279  nmoubi  21366  nmobndi  21369  nmoo0  21385  isph  21416  minvecolem4b  21473  minvecolem4  21475  minvecolem5  21476  minvecolem7  21478  h2hcau  21575  h2hlm  21576  hvaddeq0  21664  hial2eq2  21702  norm-i  21724  hhssnv  21857  shsel  21909  shsel3  21910  pjhtheu2  22011  chssoc  22091  chsscon1  22096  chpsscon1  22099  chpsscon2  22100  chlejb2  22108  elspansn2  22162  fh1  22213  fh2  22214  cm2j  22215  eigposi  22432  nmopub  22504  unopf1o  22512  nmfnleub  22521  elnlfn  22524  adjvalval  22533  lnopcnre  22635  riesz4i  22659  leop2  22720  leop3  22721  leoppos  22722  hst1h  22823  mdbr2  22892  mdbr3  22893  mdbr4  22894  dmdbr2  22899  dmdbr3  22901  dmdbr4  22902  mddmd2  22905  cvdmd  22933  atcvatlem  22981  atdmd  22994  sumdmdii  23011  dmdbr5ati  23018  cdj3lem1  23030  addltmulALT  23042  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemrv  23094  ballotlemrv1  23095  ballotlemrv2  23096  ballotlem1ri  23109  raleqbid  23147  rexeqbid  23148  reuxfr3d  23154  reuxfr4d  23155  iuneq12daf  23170  iuneq12df  23171  itgeq12dv  23211  csbcnvg  23213  xppreima  23226  abfmpeld  23233  abfmpel  23234  fmptdF  23236  fmptcof2  23244  xeqlelt  23284  cnvordtrestixx  23312  disjdsct  23384  lmxrge0  23390  lmdvg  23391  gsumpropd2lem  23394  issiga  23487  dya2ub  23590  orvcgteel  23683  derangval  23713  derangenlem  23717  subfacp1lem2a  23726  subfacp1lem5  23730  erdszelem8  23744  iccllyscon  23796  cvmsval  23812  isumgra  23882  wrdumgra  23883  iseupa  23896  eupath2lem2  23917  eupath2lem3  23918  untelirr  24069  untsucf  24071  untangtr  24075  mulcan2g  24100  mulle0b  24102  mulsuble0b  24103  zprod  24160  dfpo2  24183  dfon2lem3  24212  dfon2lem4  24213  dfon2lem7  24216  elpredim  24247  predep  24263  preduz  24271  brbtwn  24599  brcgr  24600  eqeelen  24604  brbtwn2  24605  colinearalglem1  24606  colinearalglem2  24607  colinearalglem3  24608  colinearalg  24610  axcgrid  24616  ax5seglem4  24632  ax5seglem5  24633  axbtwnid  24639  axcontlem5  24668  axcontlem7  24670  cgrcomlr  24693  ifscgr  24739  cgr3permute2  24744  cgr3permute4  24745  cgr3permute5  24746  brcolinear2  24753  brcolinear  24754  colinearperm2  24759  colinearperm4  24760  colinearperm5  24761  brofs2  24772  brifs2  24773  btwnconn1lem3  24784  btwnconn1lem4  24785  btwnconn1lem5  24786  btwnconn1lem8  24789  btwnconn1lem10  24791  btwnconn1lem11  24792  brsegle2  24804  broutsideof3  24821  outsideofeu  24826  lineunray  24842  hfninf  24888  nndivlub  24969  wl-dedlem0a  24994  ltflcei  24998  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  itg2gt0cn  25006  itgaddnclem2  25010  iblabsnclem  25014  dvreasin  25026  areacirclem2  25028  areacirclem5  25032  areacirclem6  25033  areacirc  25034  neleq12d  25036  reubidvag  25038  sbcbidv2  25072  untbi12d  25125  cnvref2  25169  feq123  25171  surjsec2  25223  inttpemp  25242  repcpwti  25264  islatalg  25286  isoriso2  25316  isdir2  25395  grpodlcan  25479  vecval3b  25555  islp3  25617  istopx  25650  prcnt  25654  cnfilca  25659  flfnei2  25680  iintlem1  25713  ismgra  25813  isalg  25824  algi  25830  dualded  25886  ismona  25912  ismonc  25917  iepiclem  25926  isepic  25927  issubcata  25949  issrc  25970  isntr  25976  islimcat  25979  prismorcset  26017  cmppar3  26077  bisig0  26165  iscol2  26196  isibg2  26213  isside1  26268  isside  26269  pdiveql  26271  abhp  26276  abhp1  26277  elicc3  26331  nn0prpwlem  26341  nn0prpw  26342  topfneec  26394  islocfin  26399  neibastop3  26414  neifg  26423  eltail  26426  filnetlem4  26433  euuni2OLD  26451  sdclem2  26555  fdc  26558  lmclim2  26577  0totbnd  26600  sstotbnd  26602  isbnd3b  26612  ismtyval  26627  isismty  26628  ismtyima  26630  heiborlem7  26644  heiborlem10  26647  bfplem1  26649  rrnmet  26656  rrnheibor  26664  ismrer1  26665  isdrngo2  26692  isidlc  26743  ralxpxfr2d  26863  elrfi  26872  elrfirn2  26874  isnacs2  26884  mrefg3  26886  nacsfix  26890  lzunuz  26950  diophin  26955  sbc2rexg  26968  sbc4rexg  26969  sbccomieg  26973  rexrabdioph  26978  4rexfrabdioph  26982  6rexfrabdioph  26983  diophren  26999  fiphp3d  27005  irrapxlem2  27011  elpell1qr2  27060  reglogltb  27079  reglogleb  27080  monotuz  27129  monotoddzz  27131  zindbi  27134  rmyeq0  27143  jm2.19lem2  27186  jm2.19lem3  27187  rmydioph  27210  expdiophlem1  27217  expdioph  27219  pw2f1o2val2  27236  soeq12d  27237  freq12d  27238  weeq12d  27239  fnwe2lem2  27251  islmodfg  27270  islssfg2  27272  dsmmelbas  27308  ellspd  27357  pwfi2f1o  27363  islindf  27385  islbs4  27405  islinds3  27407  islnr3  27422  rngunsnply  27481  f1omvdconj  27492  f1otrspeq  27493  pmtrmvd  27501  idomrootle  27614  caofcan  27643  pm14.122c  27727  pm14.123c  27730  sbaniota  27738  fnchoice  27803  rfcnpre3  27807  rfcnpre4  27808  climinf  27835  stoweidlem7  27859  stoweidlem13  27865  stoweidlem27  27879  stoweidlem34  27886  stoweidlem35  27887  stoweidlem43  27895  stoweidlem59  27911  sbcrel  28084  csbdmg  28085  sbcfun  28090  dfdfat2  28099  fnbrafvb  28122  afvelrnb  28131  dmfcoafv  28143  3bior2fd  28179  mpt2xopoveq  28201  mpt2xopovel  28202  isprmpt2  28208  isusgra0  28238  nbgrael  28275  nbusgra  28277  nbgraeledg  28279  nb3graprlem1  28287  nb3grapr2  28290  cusgra2v  28297  cusgra3vnbpr  28300  iswlk  28329  trls  28335  istrl  28336  istrl2  28337  ispth  28354  isspth  28355  0spth  28357  ispthon  28362  wlkdvspthlem  28365  0crct  28371  0cycl  28372  fargshiftfva  28384  eupatrl  28385  frgra3v  28426  trsbc  28603  sbcssOLD  28605  bnj984  29300  bnj1417  29387  islshpsm  29792  lrelat  29826  islshpat  29829  islshpcv  29865  ellkr  29901  lkr0f  29906  lkrsc  29909  lshpkrlem1  29922  islshpkrN  29932  lfl1dim  29933  lkrpssN  29975  ldual1dim  29978  ople0  29999  opltn0  30002  op1le  30004  opcon2b  30009  oplecon1b  30013  opltcon1b  30017  opltcon2b  30018  cmtvalN  30023  omllaw4  30058  cmt4N  30064  cmtbr3N  30066  cmtbr4N  30067  omlfh1N  30070  cvrval  30081  pats  30097  leatb  30104  atlle0  30117  atlltn0  30118  cvlatcvr1  30153  cvlatcvr2  30154  ishlat1  30164  glbconxN  30189  hlsupr2  30198  hlateq  30210  hlrelat  30213  hlrelat2  30214  cvrval5  30226  cvrexchlem  30230  atcvr0eq  30237  cvrat4  30254  3dim0  30268  3dim2  30279  2dim  30281  islln3  30321  llnexatN  30332  islpln3  30344  islpln5  30346  islvol3  30387  islvol5  30390  4atlem11  30420  4atlem12  30423  lineset  30549  psubspset  30555  ispsubsp2  30557  elpmapat  30575  pmapglbx  30580  isline3  30587  isline4N  30588  elpaddat  30615  elpadd2at  30617  pmapjoin  30663  dalawlem13  30694  ispsubcl2N  30758  lhpoc  30825  lhpmod2i2  30849  lhpmod6i1  30850  lautset  30893  pautsetN  30909  ltrnatb  30948  ltrnel  30950  ltrncnvel  30953  ltrneq  30960  trlid0b  30989  cdleme0ex2N  31035  cdleme3  31048  cdleme7  31060  cdlemefrs29bpre0  31207  cdlemg2cN  31400  cdlemg2cex  31402  cdlemk34  31721  cdlemkid3N  31744  cdlemkid4  31745  cdlemk39s  31750  cdlemk42  31752  dvhb1dimN  31797  diaord  31859  dia11N  31860  diaglbN  31867  dia1dim2  31874  dvhopellsm  31929  dibelval3  31959  dibopelval3  31960  dibeldmN  31970  dib11N  31972  dib1dim  31977  diblsmopel  31983  diclspsn  32006  dihopelvalbN  32050  dihopelvalcqat  32058  dihopelvalcpre  32060  xihopellsmN  32066  dihopellsm  32067  dihord3  32069  dihord4  32070  dih11  32077  dihglbcpreN  32112  dihmeetlem4preN  32118  dihlspsnat  32145  dihatexv2  32151  dochord2N  32183  dochord3  32184  dochkrshp2  32199  dihjatcclem4  32233  dihjat1lem  32240  dvh2dimatN  32252  lcfl2  32305  lcfl3  32306  lcfl4N  32307  lcfl7N  32313  lcfrvalsnN  32353  lcfrlem9  32362  lcdlss  32431  mapdordlem2  32449  mapd1o  32460  mapdcv  32472  mapdn0  32481  mapdindp  32483  mapdpglem3  32487  mapdpglem26  32510  mapdpglem27  32511  mapdpglem30  32514  mapdindp1  32532  lspindp5  32582  hdmap1ffval  32608  hdmap1fval  32609  hdmapffval  32641  hdmapfval  32642  hdmapeq0  32659  hdmap11  32663  hgmapffval  32700  hgmapfval  32701  hdmapoc  32746  hlhilphllem  32774
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