MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitrd 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 6    <-> 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  683  orbi12d  693  anbi12d  694  dedlem0a  923  ax11el  2106  eleq12d  2321  neeq12d  2427  raleqbi1dv  2696  rexeqbi1dv  2697  reueqd  2698  raleqbidv  2699  rexeqbidv  2700  raleqbidva  2701  rexeqbidva  2702  eueq3  2877  sbc19.21g  2985  sbcrext  2994  sbcabel  2998  sbcel1g  3028  sbceq1g  3029  sbcel2g  3030  sbceq2g  3031  sbccsb2g  3038  sbcco3g  3064  sseq12d  3128  psseq12d  3191  raaan  3467  raaanv  3468  elimhyp2v  3519  elimhyp4v  3521  keephyp2v  3525  ralsng  3576  rexsng  3577  ssunsn2  3673  2ralunsn  3716  csbunig  3735  disjeq12d  3899  disjprg  3916  breq123d  3934  sbcbr12g  3970  sbcbr1g  3971  sbcbr2g  3972  treq  4016  nalset  4048  copsex4g  4148  frirr  4263  ordtri1  4318  reusv7OLD  4437  reuxfr2d  4448  reuxfrd  4450  elpwun  4458  ordpwsuc  4497  ordunisuc2  4526  tfindsg  4542  dfom2  4549  findsg  4574  csbxpg  4623  posn  4665  frsn  4667  csbrng  4830  elrelimasn  4944  eliniseg  4949  brcodir  4969  fneq12d  5194  feq12d  5238  feq123d  5239  f1osng  5371  f1oprswap  5372  fv2  5373  csbfv12g  5387  csbfv12gALT  5388  dmfco  5445  eqfnfv2  5475  fndmdifeq0  5483  fneqeql2  5486  funimass3  5493  funconstss  5495  unpreima  5503  ralrnmpt  5521  dffo3  5527  fmptco  5543  fressnfv  5559  fnsuppeq0  5585  fnunirn  5630  f1elima  5639  cocan1  5653  cocan2  5654  fliftf  5666  soisores  5676  isomin  5686  isoini  5687  f1oiso  5700  f1oweALT  5703  mpt2eq123dva  5761  ovid  5816  ov  5819  ovg  5838  caovord2d  5881  ofrfval2  5948  offveqb  5951  reldm  6023  tpostpos  6106  f1ofveu  6225  oe0m1  6406  oaord1  6435  omord  6452  omlimcl  6462  oewordi  6475  oeeui  6486  nnaordr  6504  nnaordex  6522  ereq1  6553  brdifun  6573  erth2  6591  qliftfun  6629  brecop  6637  elmapg  6671  elpmg  6672  boxcutc  6745  dom2lem  6787  xpcomco  6837  pw2f1olem  6851  nndomo  6939  unfilem2  7007  domunfican  7014  indexfi  7047  elfi2  7052  supisolem  7105  hartogslem1  7141  brwdom2  7171  canthwdom  7177  infeq5i  7221  cantnfs  7251  cantnfrescl  7262  cantnfp1lem3  7266  cantnflem1b  7272  cantnflem1  7275  cnfcom3lem  7290  r1pwOLD  7402  rankxplim  7433  iscard2  7493  infxpenc2  7533  fseqenlem1  7535  fseqdom  7537  alephnbtwn  7582  alephinit  7606  iunfictbso  7625  dfac2  7641  dfac12lem2  7654  dfac12lem3  7655  kmlem2  7661  ackbij2lem2  7750  fin23lem23  7836  fin1a2lem2  7911  fin1a2lem4  7913  fin1a2lem9  7918  dcomex  7957  axdclem  8030  brdom7disj  8040  brdom6disj  8041  iundom2g  8046  axpownd  8103  fpwwe2cbv  8132  fpwwe2lem2  8134  fpwwe2lem3  8135  fpwwe2lem9  8140  fpwwe2  8145  pwfseqlem1  8160  eltskm  8345  ltapi  8407  ltmpi  8408  nlt1pi  8410  indpi  8411  nqereu  8433  ordpipq  8446  ltsonq  8473  ltanq  8475  ltrnq  8483  archnq  8484  elnpi  8492  genpass  8513  addclprlem1  8520  mulclprlem  8523  1idpr  8533  prlem934  8537  prlem936  8551  reclem4pr  8554  addgt0sr  8606  sqgt0sr  8608  ltresr  8642  leloe  8788  eqlelt  8789  negeu  8922  subadd2  8935  subcan2  8952  ltadd1  9121  leadd2  9123  ltsubadd  9124  lesubadd  9126  ltaddsub2  9129  leaddsub2  9131  ltaddpos  9144  lesub2  9149  ltnegcon1  9155  ltnegcon2  9156  lenegcon1  9158  lenegcon2  9159  addge01  9164  addge02  9165  suble0  9168  lesub0  9170  eqord2  9184  mulcan2d  9282  diveq0  9314  diveq1  9334  ltmul2  9487  lemul2  9489  ltmulgt11  9496  ltmulgt12  9497  gt0div  9502  ge0div  9503  ltmuldiv  9506  ledivmul2OLD  9514  ltdiv2  9521  ltrec1  9523  lerec2  9524  ledivdiv  9525  ltdiv23  9527  lediv23  9528  creur  9620  creui  9621  ofsubeq0  9623  nn1suc  9647  nnrecl  9842  nn0sub  9893  znnsub  9943  btwnnz  9967  gtndiv  9968  uzindOLD  9985  eluz2  10115  uzwo  10160  uzwoOLD  10161  indstr2  10175  negn0  10183  rpneg  10262  xrleloe  10357  xltadd2  10455  xsubge0  10459  xlesubadd  10461  xmulasslem  10483  xlemul2  10489  xltmul2  10491  supxrre2  10528  elixx3g  10547  ioo0  10559  iccid  10579  ico0  10580  ioc0  10581  icc0  10582  elioc2  10591  elico2  10592  elicc2  10593  elfz2  10667  fzen  10689  fzsubel  10705  fzpr  10718  fzrevral2  10745  fzrevral3  10746  fzshftral  10747  fzosplitsni  10799  btwnzge0  10831  mod0  10856  negmod0  10857  nn0ennn  10919  expeq0  11010  sq11  11054  sq01  11101  hashen  11224  hashnncl  11232  hashsdom  11241  seqcoll2  11279  ccatopth2  11340  cnpart  11602  sqrlem7  11611  sqrneglem  11629  sqabs  11669  abslt  11675  absle  11676  absdiflt  11678  absdifle  11679  lenegsq  11681  rexanuz2  11710  limsupgle  11828  limsuple  11829  clim  11845  rlim  11846  clim0c  11858  rlim0  11859  rlim0lt  11860  ello12  11867  ello1mpt  11872  elo12  11878  lo1o12  11884  elo1mpt  11885  elo1mpt2  11886  o1lo1  11888  isercolllem2  12016  isercoll2  12019  zsum  12068  fsum2dlem  12110  fsumcom2  12114  binomlem  12164  efieq  12317  sin01bnd  12339  cos01bnd  12340  divides2  12408  dvdsaddr  12442  fzocongeq  12456  odd2np1  12461  divalglem4  12469  divalglem5  12470  divalgb  12477  bits0  12493  bitsp1e  12497  bitsp1o  12498  bitscmp  12503  bitsinv1lem  12506  sadval  12521  sadcaddlem  12522  smuval  12546  smuval2  12547  dvdssq  12613  nn0seqcvgd  12614  algcvgblem  12621  isprm2  12640  qredeq  12659  prmdvdsexp  12667  prmdvdsexpb  12668  prmexpb  12670  prmfac1  12671  qnumgt0  12695  hashdvds  12717  fermltl  12726  pcpremul  12770  pc2dvds  12805  pcz  12807  prmpwdvds  12825  prmreclem5  12841  4sqlem16  12881  vdwapun  12895  vdwmc  12899  vdwlem6  12907  ramval  12929  prdsbasmpt  13243  prdsleval  13250  prdsbasmpt2  13255  imasleval  13317  xpsle  13357  mrcidb2  13392  acsfiel  13401  acsfn2  13409  catpropd  13456  cidpropd  13457  ismon2  13481  isepi2  13488  isinv  13506  isssc  13541  subsubc  13571  funcres2b  13615  funcpropd  13618  isfull  13628  isfth  13632  fullpropd  13638  isnat2  13666  fucsect  13690  fuciso  13693  elsetchom  13757  setcsect  13765  setciso  13767  evlfcl  13840  isprs  13908  isdrs  13912  posi  13928  pltval3  13945  istos  13985  islat  13997  latleeqj1  14013  latleeqj2  14014  latleeqm1  14029  latleeqm2  14030  ipodrsima  14112  isacs5  14119  isdlat  14131  ismgmid  14222  mhmpropd  14256  issubm2  14261  gsumvalx  14286  gsumpropd  14288  grpsubrcan  14382  grplactcnv  14399  issubg  14456  eqgval  14501  conjnmzb  14552  isga  14580  odmulg  14704  odf1o1  14718  odngen  14723  gexdvds  14730  pgpfi2  14752  isslw  14754  slwpss  14758  pgpssslw  14760  subgslw  14762  sylow2alem2  14764  fislw  14771  sylow3lem2  14774  lsmelvalm  14797  lsmdisj3a  14833  pj1eq  14844  iscmn  14931  eqgabl  14966  torsubg  14981  gsumval3  15026  dprdf11  15093  dprd2da  15112  dmdprdpr  15119  ablfac1eulem  15142  pgpfac1lem2  15145  pgpfac1lem3a  15146  pgpfac1lem3  15147  rngpropd  15207  dvdsrval  15262  dvdsr02  15273  unitpropd  15314  drngmuleq0  15370  drngpropd  15374  issubrg  15380  islmod  15466  lsmelpr  15679  lspsnne1  15705  fidomndrnglem  15879  coe1mul2lem2  16177  coe1tm  16181  prmirredlem  16278  prmirred  16280  domnchr  16318  znleval  16340  znchr  16348  znunithash  16350  iscss2  16418  ishil2  16451  istopg  16473  eltg  16527  eltg2  16528  tgss2  16557  bastop1  16563  bastop2  16564  iscld  16596  iscld4  16634  elcls2  16643  elcls3  16652  isclo  16656  mretopd  16661  isnei  16672  neiint  16673  neindisj2  16692  islp2  16709  maxlp  16710  cldlp  16713  iscn  16797  iscnp  16799  iscnp3  16806  tgcn  16814  subbascn  16816  ssidcn  16817  lmbr2  16821  lmbrf  16822  cnrest2  16846  hausnei2  16913  cmpsub  16959  tgcmp  16960  cmpfi  16967  consuba  16978  connsub  16979  dis2ndc  17018  subislly  17039  elkgen  17063  kgencn  17083  kgencn2  17084  eltx  17095  ptpjpre1  17098  ptcnplem  17147  hausdiag  17171  xkoptsub  17180  xkoco2cn  17184  elqtop  17220  qtopcld  17236  kqcldsat  17256  kqt0lem  17259  isr0  17260  regr1lem2  17263  ordthmeolem  17324  ptuncnv  17330  trfbas  17371  elfg  17398  trfil3  17415  trufil  17437  filufint  17447  uffix2  17451  elfm2  17475  elfm3  17477  flimtopon  17497  flimopn  17502  fbflim  17503  fbflim2  17504  flffbas  17522  flftg  17523  cnflf  17529  txflf  17533  isfcls  17536  fclstopon  17539  fclsbas  17548  fclsrest  17551  fcfnei  17562  cnfcf  17569  ptcmplem2  17579  tgphaus  17631  tgpt0  17633  divstgphaus  17637  tsmsgsum  17653  tsmsres  17658  tsmsxplem1  17667  ismet  17720  isxmet  17721  metn0  17756  xmetres2  17757  elbl3  17783  xblpnf  17785  elmopn2  17823  metss  17886  stdbdxmet  17893  metcnp3  17918  metcnp  17919  metcnp2  17920  metcn  17921  txmetcnp  17925  txmetcn  17926  dscopn  17928  isngp3  17952  nmeq0  17971  ngppropd  17985  isnghm3  18066  isnmhm2  18093  bl2ioo  18130  metdsge  18185  metnrmlem1a  18194  addcnlem  18200  elcncf  18225  elcncf2  18226  evth  18289  elpi1  18375  nmhmcn  18433  cphipeq0  18471  ipcau2  18496  lmmbr  18516  lmmbr2  18517  iscfil2  18524  fmcfil  18530  iscau  18534  iscau2  18535  iscau3  18536  iscau4  18537  iscauf  18538  caucfil  18541  metcld2  18564  bcthlem1  18578  lssbn  18605  srabn  18609  ishl2  18619  minveclem7  18631  ivth2  18647  ovolfioo  18659  ovolficc  18660  ovolshftlem1  18700  ovolicc2lem1  18708  icombl  18753  ioombl  18754  volsup2  18792  ismbf  18817  ismbfcn  18818  ismbfcn2  18826  mbfmax  18836  mbfimaopnlem  18842  mbfaddlem  18847  mbfsup  18851  mbfinf  18852  mbflimsup  18853  i1faddlem  18880  i1fres  18892  itg1ge0a  18898  itg1climres  18901  mbfi1fseqlem4  18905  itg2leub  18921  itg2const  18927  itg2split  18936  itg2cnlem2  18949  iblcnlem1  18974  iblrelem  18977  itgss3  19001  ellimc  19055  ellimc2  19059  ellimc3  19061  limcmpt  19065  limcmpt2  19066  limcres  19068  cnplimc  19069  limcun  19077  dvreslem  19091  dvcnp  19100  dvcnvlem  19155  dveflem  19158  cmvth  19170  mdegleb  19282  mdegldg  19284  degltp1le  19291  mdegle0  19295  deg1ldg  19310  coe1mul3  19317  ply1remlem  19380  fta1glem2  19384  ply1termlem  19417  coemulc  19468  coecj  19491  plymul0or  19493  ofmulrt  19494  quotval  19504  plydivlem4  19508  plyremlem  19516  ulmcau2  19605  reeff1o  19655  sincosq2sgn  19699  sinq12gt0  19707  coseq1  19722  logltb  19785  cosarg0d  19795  argrege0  19797  tanarg  19802  affineequiv  19955  dcubic1lem  19971  dcubic  19974  atandm2  20005  rlimcnp  20092  rlimcnp2  20093  xrlimcnp  20095  fsumharmonic  20137  wilthlem1  20138  ftalem7  20148  basellem3  20152  isppw2  20185  issqf  20206  sqf11  20209  mumullem2  20250  sqff1o  20252  muinv  20265  ppiublem1  20273  vmasum  20287  chpchtsum  20290  chpub  20291  dchrelbas2  20308  dchrelbas3  20309  dchrelbas4  20314  dchrinv  20332  efexple  20352  bposlem1  20355  bposlem6  20360  bposlem7  20361  lgsdilem  20393  lgsdir2lem4  20397  lgsdir2  20399  lgsne0  20404  lgsabs1  20405  lgsquad3  20432  2sqlem7  20441  2sqlem8a  20442  chtppilim  20456  dchrvmaeq0  20485  dirith  20510  ostth3  20619  isgrpo  20693  isablo  20780  ismgm  20817  opidon2  20821  ismndo1  20841  elghomlem2  20859  isrngo  20875  iscom2  20909  rngosn3  20923  rngosn4  20924  vci  20934  isvclem  20963  vcoprnelem  20964  nvsubadd  21043  nvelbl  21092  nvelbl2  21093  nmoubi  21180  nmobndi  21183  nmoo0  21199  isph  21230  minvecolem4b  21287  minvecolem4  21289  minvecolem5  21290  minvecolem7  21292  h2hcau  21389  h2hlm  21390  hvaddeq0  21478  hial2eq2  21516  norm-i  21538  hhssnv  21671  shsel  21723  shsel3  21724  pjhtheu2  21825  chssoc  21905  chsscon1  21910  chpsscon1  21913  chpsscon2  21914  chlejb2  21922  elspansn2  21976  fh1  22045  fh2  22046  cm2j  22047  eigposi  22246  nmopub  22318  unopf1o  22326  nmfnleub  22335  elnlfn  22338  adjvalval  22347  lnopcnre  22449  riesz4i  22473  leop2  22534  leop3  22535  leoppos  22536  hst1h  22637  mdbr2  22706  mdbr3  22707  mdbr4  22708  dmdbr2  22713  dmdbr3  22715  dmdbr4  22716  mddmd2  22719  cvdmd  22747  atcvatlem  22795  atdmd  22808  sumdmdii  22825  dmdbr5ati  22832  cdj3lem1  22844  addltmulALT  22856  derangval  22869  derangenlem  22873  subfacp1lem2a  22882  subfacp1lem5  22886  erdszelem8  22900  iccllyscon  22952  cvmsval  22968  isumgra  23038  wrdumgra  23039  iseupa  23052  eupath2lem2  23073  eupath2lem3  23074  untelirr  23225  untsucf  23227  untangtr  23231  mulcan2g  23255  mulle0b  23257  mulsuble0b  23258  dfpo2  23282  dfon2lem3  23309  dfon2lem4  23310  dfon2lem7  23313  elpredim  23344  predep  23360  preduz  23368  brbtwn  23701  brcgr  23702  eqeelen  23706  brbtwn2  23707  colinearalglem1  23708  colinearalglem2  23709  colinearalglem3  23710  colinearalg  23712  axcgrid  23718  ax5seglem4  23734  ax5seglem5  23735  axbtwnid  23741  axcontlem5  23770  axcontlem7  23772  cgrcomlr  23795  ifscgr  23841  cgr3permute2  23846  cgr3permute4  23847  cgr3permute5  23848  brcolinear2  23855  brcolinear  23856  colinearperm2  23861  colinearperm4  23862  colinearperm5  23863  brofs2  23874  brifs2  23875  btwnconn1lem3  23886  btwnconn1lem4  23887  btwnconn1lem5  23888  btwnconn1lem8  23891  btwnconn1lem10  23893  btwnconn1lem11  23894  brsegle2  23906  broutsideof3  23923  outsideofeu  23928  lineunray  23944  hfninf  23990  nndivlub  24071  wl-dedlem0a  24096  neleq12d  24098  reubidvag  24100  sbcbidv2  24134  untbi12d  24187  cnvref2  24231  feq123  24233  surjsec2  24286  inttpemp  24305  repcpwti  24327  islatalg  24349  isoriso2  24379  isdir2  24458  grpodlcan  24542  vecval3b  24618  islp3  24680  istopx  24713  prcnt  24717  cnfilca  24722  flfnei2  24743  iintlem1  24776  ismgra  24876  isalg  24887  algi  24893  dualded  24949  ismona  24975  ismonc  24980  iepiclem  24989  isepic  24990  issubcata  25012  issrc  25033  isntr  25039  islimcat  25042  prismorcset  25080  cmppar3  25140  bisig0  25228  iscol2  25259  isibg2  25276  isside1  25331  isside  25332  pdiveql  25334  abhp  25339  abhp1  25340  elicc3  25394  nn0prpwlem  25404  nn0prpw  25405  topfneec  25457  islocfin  25462  neibastop3  25477  neifg  25486  eltail  25489  filnetlem4  25496  euuni2OLD  25514  sdclem2  25618  fdc  25621  lmclim2  25640  0totbnd  25663  sstotbnd  25665  isbnd3b  25675  ismtyval  25690  isismty  25691  ismtyima  25693  heiborlem7  25707  heiborlem10  25710  bfplem1  25712  rrnmet  25719  rrnheibor  25727  ismrer1  25728  isdrngo2  25755  isidlc  25806  ralxpxfr2d  25926  elrfi  25935  elrfirn2  25937  isnacs2  25947  mrefg3  25949  nacsfix  25953  lzunuz  26013  diophin  26018  sbc2rexg  26031  sbc4rexg  26032  sbccomieg  26036  rexrabdioph  26041  4rexfrabdioph  26045  6rexfrabdioph  26046  diophren  26062  fiphp3d  26068  irrapxlem2  26074  elpell1qr2  26123  reglogltb  26142  reglogleb  26143  monotuz  26192  monotoddzz  26194  zindbi  26197  rmyeq0  26206  jm2.19lem2  26249  jm2.19lem3  26250  rmydioph  26273  expdiophlem1  26280  expdioph  26282  pw2f1o2val2  26299  soeq12d  26300  freq12d  26301  weeq12d  26302  fnwe2lem2  26314  islmodfg  26333  islssfg2  26335  dsmmelbas  26371  ellspd  26420  pwfi2f1o  26426  islindf  26448  islbs4  26468  islinds3  26470  islnr3  26485  rngunsnply  26544  f1omvdconj  26555  f1otrspeq  26556  pmtrmvd  26564  idomrootle  26677  caofcan  26706  pm14.122c  26791  pm14.123c  26794  sbaniota  26802  fnchoice  26867  rfcnpre3  26871  rfcnpre4  26872  stoweidlem7  26890  stoweidlem13  26896  stoweidlem27  26910  stoweidlem34  26917  stoweidlem35  26918  stoweidlem43  26926  stoweidlem59  26942  trsbc  27094  sbcss  27096  bnj984  27770  bnj1417  27857  islshpsm  28074  lrelat  28108  islshpat  28111  islshpcv  28147  ellkr  28183  lkr0f  28188  lkrsc  28191  lshpkrlem1  28204  islshpkrN  28214  lfl1dim  28215  lkrpssN  28257  ldual1dim  28260  ople0  28281  opltn0  28284  op1le  28286  opcon2b  28291  oplecon1b  28295  opltcon1b  28299  opltcon2b  28300  cmtvalN  28305  omllaw4  28340  cmt4N  28346  cmtbr3N  28348  cmtbr4N  28349  omlfh1N  28352  cvrval  28363  pats  28379  leatb  28386  atlle0  28399  atlltn0  28400  cvlatcvr1  28435  cvlatcvr2  28436  ishlat1  28446  glbconxN  28471  hlsupr2  28480  hlateq  28492  hlrelat  28495  hlrelat2  28496  cvrval5  28508  cvrexchlem  28512  atcvr0eq  28519  cvrat4  28536  3dim0  28550  3dim2  28561  2dim  28563  islln3  28603  llnexatN  28614  islpln3  28626  islpln5  28628  islvol3  28669  islvol5  28672  4atlem11  28702  4atlem12  28705  lineset  28831  psubspset  28837  ispsubsp2  28839  elpmapat  28857  pmapglbx  28862  isline3  28869  isline4N  28870  elpaddat  28897  elpadd2at  28899  pmapjoin  28945  dalawlem13  28976  ispsubcl2N  29040  lhpoc  29107  lhpmod2i2  29131  lhpmod6i1  29132  lautset  29175  pautsetN  29191  ltrnatb  29230  ltrnel  29232  ltrncnvel  29235  ltrneq  29242  trlid0b  29271  cdleme0ex2N  29317  cdleme3  29330  cdleme7  29342  cdlemefrs29bpre0  29489  cdlemg2cN  29682  cdlemg2cex  29684  cdlemk34  30003  cdlemkid3N  30026  cdlemkid4  30027  cdlemk39s  30032  cdlemk42  30034  dvhb1dimN  30079  diaord  30141  dia11N  30142  diaglbN  30149  dia1dim2  30156  dvhopellsm  30211  dibelval3  30241  dibopelval3  30242  dibeldmN  30252  dib11N  30254  dib1dim  30259  diblsmopel  30265  diclspsn  30288  dihopelvalbN  30332  dihopelvalcqat  30340  dihopelvalcpre  30342  xihopellsmN  30348  dihopellsm  30349  dihord3  30351  dihord4  30352  dih11  30359  dihglbcpreN  30394  dihmeetlem4preN  30400  dihlspsnat  30427  dihatexv2  30433  dochord2N  30465  dochord3  30466  dochkrshp2  30481  dihjatcclem4  30515  dihjat1lem  30522  dvh2dimatN  30534  lcfl2  30587  lcfl3  30588  lcfl4N  30589  lcfl7N  30595  lcfrvalsnN  30635  lcfrlem9  30644  lcdlss  30713  mapdordlem2  30731  mapd1o  30742  mapdcv  30754  mapdn0  30763  mapdindp  30765  mapdpglem3  30769  mapdpglem26  30792  mapdpglem27  30793  mapdpglem30  30796  mapdindp1  30814  lspindp5  30864  hdmap1ffval  30890  hdmap1fval  30891  hdmapffval  30923  hdmapfval  30924  hdmapeq0  30941  hdmap11  30945  hgmapffval  30982  hgmapfval  30983  hdmapoc  31028  hlhilphllem  31056
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator