MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylbi Unicode version

Theorem sylbi 188
Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
sylbi.1  |-  ( ph  <->  ps )
sylbi.2  |-  ( ps 
->  ch )
Assertion
Ref Expression
sylbi  |-  ( ph  ->  ch )

Proof of Theorem sylbi
StepHypRef Expression
1 sylbi.1 . . 3  |-  ( ph  <->  ps )
21biimpi 187 . 2  |-  ( ph  ->  ps )
3 sylbi.2 . 2  |-  ( ps 
->  ch )
42, 3syl 16 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  bi2  190  3imtr4i  258  sylnbi  298  imp  419  an12s  777  an32s  780  an4s  800  oibabs  852  jaoi2  934  3simpb  955  3simpc  956  3imp  1147  3com12  1157  3com13  1158  syl3anb  1227  19.33b  1615  exintrbi  1620  ax17e  1625  spimfw  1653  sp  1759  a6e  1763  nfr  1773  19.9t  1789  nfnd  1805  nfndOLD  1806  equs5eOLD  1907  exdistrf  2028  equviniOLD  2041  equveliOLD  2043  ax10-16  2240  euex  2277  eumo0  2278  mopick  2316  2euex  2326  2mo  2332  2eu3  2336  exists2  2344  eqcoms  2407  eleq2s  2496  nfcr  2532  necon3bi  2608  necon1ai  2609  necon2ai  2612  pm2.61ne  2642  pm2.61ine  2643  rexex  2725  rsp  2726  ralim  2737  r19.36av  2816  r19.37  2817  r19.44av  2824  r19.45av  2825  gencl  2944  gencbvex  2958  vtoclgf  2970  pm13.183  3036  elrabi  3050  mo2icl  3073  mob2  3074  reu3  3084  rmoim  3093  2reuswap  3096  sbcex  3130  ra5  3205  sseq1  3329  unineq  3551  dfrab3ss  3579  reldisj  3631  disjel  3634  pssdif  3650  difin0ss  3654  uneqdifeq  3676  r19.2z  3677  r19.3rz  3679  r19.3rzv  3681  ralidm  3691  ifnefalse  3707  ifbi  3716  nelpri  3795  rabrsn  3834  prprc1  3874  difprsn2  3896  diftpsn3  3897  tpprceq3  3898  tppreqb  3899  pwpw0  3906  ssunsn2  3918  snsssn  3927  preqr2  3933  preq12b  3934  opthpr  3936  prneimg  3938  pwsnALT  3970  intmin4  4039  dfiin2g  4084  iinss2  4103  invdisj  4161  disjiun  4162  trel  4269  trss  4271  trint0  4279  axrep5  4285  zfrep4  4288  ssex  4307  intex  4316  intnex  4317  intabs  4321  abssexg  4344  axpr  4362  rext  4372  unipw  4374  moabex  4382  nnullss  4385  exss  4386  copsexg  4402  pwssun  4449  epelg  4455  solin  4486  elsuci  4607  sucprc  4616  ordsssuc2  4629  ordssun  4640  ordequn  4641  onun2i  4656  reusv2lem1  4683  reusv2lem4  4686  reusv3  4690  reusv5OLD  4692  elpwunsn  4716  onmindif2  4751  suceloni  4752  ordpwsuc  4754  onsucmin  4760  ordsucelsuc  4761  ordsucun  4764  unon  4770  ordunisuc  4771  0elsuc  4774  onuninsuci  4779  orduninsuc  4782  limsuc  4788  limuni3  4791  tfi  4792  tfindsg  4799  limomss  4809  limom  4819  find  4829  findsg  4831  0nelelxp  4866  opelxp  4867  elvvuni  4897  posn  4905  frsn  4907  optocl  4911  xpsspwOLD  4946  ralxpf  4978  relop  4982  breldm  5033  elreldm  5053  dmrnssfld  5088  dmcosseq  5096  resabs1  5134  resima2  5138  relimasn  5186  issref  5206  asymref  5209  asymref2  5210  xpidtr  5215  trin2  5216  poirr2  5217  xpnz  5251  xp11  5263  xpcan  5264  xpcan2  5265  cnveqb  5285  dfco2a  5329  cores2  5341  coi2  5345  relcnvtr  5348  relresfld  5355  unixp0  5362  unixpid  5363  relcnvexb  5366  iotauni  5389  iota1  5391  iota4  5395  dffun8  5439  funcnvsn  5455  imadif  5487  fcoi1  5576  fcoi2  5577  f1ocnv  5646  f1ocnvb  5647  fun11iun  5654  ffoss  5666  f1o00  5669  fo00  5670  nfunsn  5720  fvfundmfvn0  5721  fnrnfv  5732  ssimaex  5747  dffv2  5755  fvmptss  5772  fvmptss2  5783  fvimacnv  5804  unpreima  5815  respreima  5818  elrnrexdm  5833  elrnrexdmb  5834  eldmrexrnb  5836  dffo4  5844  exfo  5846  rnmptss  5856  funressn  5878  fvpr1  5894  fvpr2  5895  fvpr1g  5896  fvtp1  5898  fvtp1g  5901  fconst5  5908  eufnfv  5931  elunirnALT  5959  f1veqaeq  5964  isores1  6013  f1oweALT  6033  oprabid  6064  0neqopab  6078  brabv  6079  oprssdm  6187  1stval2  6323  2ndval2  6324  fo1stres  6329  fo2ndres  6330  1st2val  6331  2nd2val  6332  xp1st  6335  xp2nd  6336  unielxp  6344  releldm2  6356  bropopvvv  6385  cnvf1o  6404  fo2ndf  6412  frxp  6415  poxp  6417  mpt2xopxnop0  6425  brovex  6433  reldmtpos  6446  dftpos4  6457  tpostpos  6458  tpostpos2  6459  sorpssun  6488  sorpssin  6489  sorpssuni  6490  sorpssint  6491  opabiota  6497  riotauni  6515  riotacl2  6522  riota1  6527  riota1a  6528  snriota  6539  eusvobj2  6541  iunon  6559  iinon  6561  smoel  6581  tfrlem4  6599  tfrlem5  6600  tfrlem7  6603  tfrlem8  6604  tfrlem9  6605  tfr2b  6616  rdgsucg  6640  frsuc  6653  tz7.48lem  6657  tz7.48-1  6659  tz7.49  6661  abianfp  6675  oesuclem  6728  oaord  6749  nnaord  6821  nneob  6854  ecexr  6869  swoord1  6893  swoord2  6894  0er  6899  ecdmn0  6906  mapprc  6981  mapsnconst  7018  ixpprc  7042  ixpf  7043  ixpn0  7053  ixp0  7054  undifixp  7057  mptelixpg  7058  boxriin  7063  idssen  7111  ener  7113  en0  7129  en1  7133  en1b  7134  2dom  7138  snfi  7146  xpsnen  7151  sbthlem1  7176  sbthlem10  7185  domnsym  7192  2pwuninel  7221  ssenen  7240  php  7250  php3  7252  ominf  7280  isinf  7281  pssnn  7286  ssfi  7288  enp1i  7302  findcard  7306  findcard2  7307  findcard3  7309  difinf  7336  infcntss  7339  fiint  7342  pwfi  7360  elfiun  7393  card2on  7478  brwdomn0  7493  unwdomg  7508  unxpwdom2  7512  ixpiunwdom  7515  sucprcreg  7523  inf0  7532  inf3lem1  7539  infeq5i  7547  infeq5  7548  dfom3  7558  trcl  7620  epfrs  7623  setind2  7630  tz9.12lem3  7671  rankwflemb  7675  rankf  7676  rankidb  7682  snwf  7691  uniwf  7701  rankpwi  7705  rankunb  7732  rankuni2b  7735  rankuni  7745  rankxpsuc  7762  tcrank  7764  scottex  7765  scott0  7766  bnd2  7773  karden  7775  finnum  7791  carduni  7824  cardiun  7825  dif1card  7848  infxpenlem  7851  fseqenlem2  7862  acnrcl  7879  acndom  7888  acnnum  7889  alephfp  7945  iunfictbso  7951  dfac4  7959  dfac5lem4  7963  dfac5  7965  dfac2  7967  dfac9  7972  dfac12r  7982  kmlem2  7987  kmlem4  7989  kmlem12  7997  kmlem13  7998  ackbij2  8079  cardcf  8088  cfeq0  8092  cfsuc  8093  alephsing  8112  fin4en1  8145  enfin2i  8157  fin23lem16  8171  fin23lem21  8175  fin23lem29  8177  fin23lem30  8178  fin23lem40  8187  isfin32i  8201  isfin1-2  8221  fin34  8226  fin45  8228  fin17  8230  fin67  8231  isfin7-2  8232  fin1a2lem7  8242  fin1a2lem10  8245  fin1a2lem12  8247  itunitc  8257  axcc4dom  8277  dcomex  8283  axdc3lem4  8289  axdc4lem  8291  axcclem  8293  ac6c4  8317  ac6sf  8325  ac6s4  8326  zorn2lem6  8337  zorn2lem7  8338  zorng  8340  zornn0g  8341  ttukeylem6  8350  ttukey2g  8352  brdom5  8363  brdom4  8364  unirnfdomd  8398  alephval2  8403  alephadd  8408  alephmul  8409  alephsuc3  8411  alephexp2  8412  alephreg  8413  pwcfsdom  8414  cfpwsdom  8415  fpwwe2lem8  8468  gchinf  8488  pwfseq  8495  winaon  8519  winacard  8523  winainf  8525  tsk0  8594  tskcard  8612  r1tskina  8613  gruima  8633  intgru  8645  ingru  8646  gruina  8649  axgroth6  8659  grothomex  8660  indpi  8740  nqereu  8762  nqerf  8763  ordpipq  8775  prn0  8822  prpssnq  8823  nqpr  8847  ltexprlem4  8872  reclem2pr  8881  mulcmpblnr  8905  recexsrlem  8934  map2psrpr  8941  supsr  8943  axpre-sup  9000  1re  9046  renfdisj  9094  ltxrlt  9102  lemul1a  9820  ltdiv2OLD  9852  sup3  9921  supmul1  9929  supmullem1  9930  supmul  9932  peano2nn  9968  nn0ge0  10203  elnnnn0b  10220  nn0sub  10226  znegcl  10269  zeo  10311  nn0ind  10322  nn0ind-raph  10326  uzn0  10457  eluzaddi  10468  eluzsubi  10469  uznn0sub  10473  uznnssnn  10480  uz2m1nn  10506  uz2mulcl  10509  indstr2  10510  qmulz  10533  qre  10535  qnegcl  10547  qreccl  10550  rphalflt  10594  xrltnr  10676  xnegcl  10755  xnegneg  10756  xltnegi  10758  xnegid  10778  xaddid1  10781  xmulid1  10814  xrsupsslem  10841  xrinfmsslem  10842  xrsupss  10843  xrinfmss  10844  elioore  10902  ioorebas  10962  elfzuz2  11018  fzn0  11026  fzdisj  11034  fzon0  11111  fzoss1  11117  elfznelfzo  11147  elfznelfzob  11148  fzind2  11153  injresinjlem  11154  injresinj  11155  om2uzrani  11247  uzrdgfni  11253  fzfi  11266  expcl2lem  11348  crreczi  11459  nn0opthlem2  11517  nn0opthi  11518  facp1  11526  facnn2  11530  faclbnd3  11538  faclbnd4lem1  11539  faclbnd4lem3  11541  bcn1  11559  hashnn0pnf  11581  hashnnn0genn0  11582  hashnemnf  11583  hashv01gt1  11584  hashrabrsn  11603  hashunx  11615  elprchashprn2  11622  hash1snb  11636  hashgt12el  11637  hashgt12el2  11638  hash2prde  11643  hashtpg  11646  hashfun  11655  hashf1lem2  11660  brfi1uzind  11670  iswrdi  11686  wrdf  11688  swrd00  11720  swrdcl  11721  rexanuz  12104  fclim  12302  climmo  12306  rlimdiv  12394  caurcvg2  12426  fsum2dlem  12509  fsumcom2  12513  arisum  12594  arisum2  12595  ef01bndlem  12740  sin01gt0  12746  cos01gt0  12747  sin02gt0  12748  xpnnenOLD  12764  odd2np1  12863  divalglem1  12869  divalglem6  12873  ndvdsadd  12883  gcdaddmlem  12983  mulgcd  13001  algcvgblem  13023  algfx  13026  prmind2  13045  maxprmfct  13068  dfphi2  13118  pythagtriplem2  13146  pcz  13209  prmunb  13237  prmreclem3  13241  4sqlem4  13275  4sqlem19  13286  ramz  13348  firest  13615  imasaddfnlem  13708  xpsfrnel2  13745  mreiincl  13776  mreunirn  13781  mremre  13784  fnmrc  13787  mrcfval  13788  ismon2  13915  isepi2  13922  sscpwex  13970  funcres2b  14049  funcpropd  14052  funcres2c  14053  isfull  14062  isfth  14066  homa1  14147  homahom2  14148  cnvpsb  14600  spwmo  14613  laspwcl  14621  lanfwcl  14622  gsumval2  14738  subgint  14919  giclcl  15014  gicrcl  15015  gicsym  15016  gicen  15019  gicsubgen  15020  cntzssv  15082  oppgsubm  15113  oppgsubg  15114  gexcl3  15176  sylow3lem6  15221  efgmnvl  15301  efgsf  15316  efgsrel  15321  efgs1b  15323  efgredlema  15327  efgredlemd  15331  efgrelexlema  15336  efgrelexlemb  15337  frgpnabllem1  15439  cygabl  15455  cyggex2  15461  giccyg  15464  dprdval  15516  dprdssv  15529  pgpfac1  15593  dvdsrval  15705  isunit  15717  drngmuleq0  15813  opprsubrg  15844  subrgint  15845  lmhmlem  16060  lmiclcl  16097  lmicrcl  16098  lmicsym  16099  lvecvscan  16138  lspsncv0  16173  abvn0b  16317  evlslem4  16519  cnsubdrglem  16704  prmirred  16730  zlmlmod  16759  frgpcyg  16809  thlle  16879  tgiun  16999  distop  17015  ssntr  17077  isclo2  17107  indiscld  17110  neiptopuni  17149  lecldbas  17237  pnfnei  17238  mnfnei  17239  lmrcl  17249  cmpsublem  17416  cmpsub  17417  hauscmplem  17423  iuncon  17444  2ndctop  17463  2ndcsb  17465  2ndcredom  17466  2ndc1stc  17467  2ndcdisj  17472  2ndcsep  17475  kgenuni  17524  kgenftop  17525  kgenss  17528  kgenidm  17532  iskgen3  17534  kgencn3  17543  txuni2  17550  dfac14  17603  txcn  17611  txindis  17619  kqtop  17730  kqt0  17731  hmeocnvb  17759  hmphref  17766  hmphsym  17767  hmphen  17770  haushmphlem  17772  cmphmph  17773  conhmph  17774  reghmph  17778  nrmhmph  17779  hmphdis  17781  hmphindis  17782  indishmph  17783  hmphen2  17784  ist1-5lem  17805  fbncp  17824  isfil2  17841  fbasfip  17853  fgcl  17863  filunirn  17867  cfinfil  17878  fiufl  17901  ufinffr  17914  isfcls  17994  alexsubALTlem2  18032  alexsubALTlem3  18033  tmdcn2  18072  ustbas  18210  psmettri2  18293  xmetunirn  18320  lpbl  18486  blcld  18488  met1stc  18504  met2ndci  18505  dscmet  18573  qdensere  18757  blssioo  18779  xrtgioo  18790  divcn  18851  iimulcl  18915  iimulcn  18916  iccpnfcnv  18922  isphtpc  18972  phtpc01  18974  cmetcaulem  19194  bcthlem4  19233  elovolm  19324  ovolmge0  19326  ovolgelb  19329  ovolfi  19343  iunmbl  19400  iunmbl2  19404  ioombl1  19409  ioorcl2  19417  ioorf  19418  ioorinv2  19420  ioorinv  19421  ioorcl  19422  dyaddisj  19441  dyadmax  19443  opnmblALT  19448  vitali  19458  mbfid  19481  itg1addlem4  19544  itg2uba  19588  itg2splitlem  19593  limcdif  19716  ellimc2  19717  limcres  19726  limccnp  19731  dvexp2  19793  dvexp3  19815  mpfrcl  19892  pf1rcl  19922  pf1ind  19928  elply2  20068  plyssc  20072  elqaa  20192  aannenlem1  20198  aannenlem2  20199  aannenlem3  20200  aaliou2  20210  taylfval  20228  ulmscl  20248  pserdvlem2  20297  reeff1o  20316  sincosq1sgn  20359  sincosq2sgn  20360  sincosq3sgn  20361  sincosq4sgn  20362  sinq12gt0  20368  logfac  20448  dvloglem  20492  logf1o2  20494  logtayl  20504  cxpexp  20512  resqrcn  20586  reasinsin  20689  birthdaylem1  20743  harmonicbnd3  20799  sqff1o  20918  musum  20929  bpos1  21020  2sqlem2  21101  2sqlem10  21111  chebbnd1  21119  chtppilim  21122  chpo1ub  21127  dchrisum0lem2a  21164  rplogsum  21174  pnt2  21260  ostth  21286  uhgra0v  21298  ausisusgra  21333  usgraedgprv  21349  usgraedgrnv  21350  usgra2edg  21355  usgrarnedg  21357  usgraedg4  21359  usgra1v  21362  usgraidx2v  21365  usgraexmpl  21373  usgrafisindb0  21375  usgrares1  21377  nbgra0nb  21394  nbgranself  21399  nbgrassovt  21400  nbgranself2  21401  nbgraf1olem1  21404  nb3graprlem1  21413  nb3graprlem2  21414  cusgrarn  21421  cusgra1v  21423  nbcusgra  21425  cusgrafilem2  21442  wlkntrllem3  21514  wlkntrl  21515  0spth  21524  spthonepeq  21540  wlkdvspthlem  21560  fargshiftf1  21577  usgrcyclnl1  21580  usgrcyclnl2  21581  3v3e3cycl1  21584  constr3lem6  21589  constr3trllem2  21591  3v3e3cycl2  21604  4cycl4v4e  21606  4cycl4dv4e  21608  1conngra  21615  vdgrf  21622  vdusgraval  21631  eupatrl  21643  eupath  21656  grposn  21756  gxsuc  21813  ismgm  21861  isexid2  21866  ablomul  21896  rngo1cl  21970  nmobndseqi  22233  nmobndseqiOLD  22234  ipasslem5  22289  h2hcau  22435  hvsubeq0i  22518  hvmulcan  22527  hvmulcan2  22528  bcsiALT  22634  hhcms  22658  hlimf  22693  isch3  22697  hsn0elch  22703  hhssnv  22717  shintcli  22784  hsupcl  22794  hsupunss  22798  sshjcl  22810  shsleji  22825  shsidmi  22839  hsupval2  22864  sshjval2  22866  spanuni  22999  h1de2i  23008  spanunsni  23034  cmbr3i  23055  osumcor2i  23099  spansncvi  23107  5oalem7  23115  3oalem3  23119  pjss2i  23135  pjssmii  23136  mayete3i  23183  mayete3iOLD  23184  nmop0h  23447  riesz3i  23518  nmopcoi  23551  opsqrlem5  23600  pjnmopi  23604  pjorthcoi  23625  pjssdif1i  23631  dfpjop  23638  elpjch  23645  pjin2i  23649  pjclem1  23651  pjclem2  23652  pjclem4a  23654  pj3lem1  23662  strlem1  23706  strlem3  23709  strlem4  23710  strlem5  23711  stri  23713  hstrlem3  23717  hstrlem4  23718  hstrlem5  23719  hstri  23721  stcltr1i  23730  dmdbr5  23764  mdsl1i  23777  mdslmd1lem2  23782  atne0  23801  atom1d  23809  shatomici  23814  chrelat2i  23821  atssma  23834  chirredi  23850  cmmdi  23872  sumdmdi  23876  dmdbr4ati  23877  dmdbr5ati  23878  dmdbr6ati  23879  dmdbr7ati  23880  cdj3lem1  23890  2reuswap2  23928  rexunirn  23931  elim2ifim  23959  iuninc  23964  fimacnvinrn  24000  unipreima  24009  xppreima  24012  xrofsup  24079  xrge0iifcnv  24272  xrge0iifiso  24274  xrge0iifhom  24276  logbcl  24350  esumc  24399  esumpinfval  24416  hasheuni  24428  ofcfval  24434  sigaclfu  24455  volmeas  24540  truae  24547  sxbrsigalem0  24574  dya2icobrsiga  24579  dya2iocucvr  24587  sxbrsigalem2  24589  ballotlem2  24699  ballotlem7  24746  igamgam  24786  subfacval3  24828  erdszelem2  24831  kur14lem7  24851  kur14lem9  24853  m1expevenALT  24858  rellyscon  24891  cvmliftlem15  24938  cvmlift2lem12  24954  ghomgrpilem2  25050  untangtr  25116  dedekind  25140  dedekindle  25141  fz0n  25155  prodmo  25215  fprodfac  25249  fprod2dlem  25257  fprodcom2  25261  br8  25327  br6  25328  br4  25329  eldm3  25333  fununiq  25340  setinds  25348  setinds2f  25349  dfon2lem3  25355  dfon2lem7  25359  dfon2lem8  25360  rdgprc0  25364  dfrdg2  25366  elpredim  25390  prednn  25415  tfisg  25418  wfisg  25423  nnsinds  25431  nn0sinds  25432  trpredmintr  25448  trpredrec  25455  frmin  25456  frinsg  25459  soseq  25468  wfrlem2  25471  wfrlem3  25472  wfrlem4  25473  wfrlem9  25478  wfrlem11  25480  wfrlem12  25481  frrlem2  25496  frrlem3  25497  frrlem4  25498  frrlem5c  25501  frrlem5e  25503  frrlem11  25507  nofun  25517  nodmon  25518  norn  25519  sltval2  25524  sltsgn1  25529  sltsgn2  25530  sltintdifex  25531  sltres  25532  nofulllem5  25574  txpss3v  25632  pprodss4v  25638  fnimage  25682  imageval  25683  dfrdg4  25703  altopthsn  25710  altxpsspw  25726  axlowdimlem13  25797  axlowdim1  25802  axcontlem4  25810  linethru  25991  bpoly2  26007  bpoly3  26008  bpoly4  26009  rankeq1o  26016  waj-ax  26068  amosym1  26080  ordtoplem  26089  onsucconi  26091  onintopsscon  26094  onsuct0  26095  limsucncmpi  26099  ordcmp  26101  onint1  26103  mblfinlem2  26144  ismblfin  26146  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  mbfposadd  26153  itg2addnclem  26155  itgaddnclem2  26163  dvreasin  26179  areacirclem2  26181  areacirclem5  26185  finminlem  26211  nn0prpwlem  26215  nn0prpw  26216  cldbnd  26219  fnemeet2  26286  fdc  26339  subspopn  26348  sstotbnd3  26375  totbndbnd  26388  heiborlem3  26412  heiborlem8  26417  exidcl  26441  riscer  26494  divrngidl  26528  smprngopr  26552  prtlem9  26603  prtlem16  26608  prtlem14  26613  fndifnfp  26627  cmpfiiin  26641  ismrcd1  26642  isnacs3  26654  fzsplit1nn0  26702  eldiophss  26723  2nn0ind  26898  jm2.23  26957  expdiophlem1  26982  expdioph  26984  setindtrs  26986  dfac11  27028  lnmlmic  27054  gicabl  27131  isnumbasgrplem2  27137  dfacbasgrp  27141  lindfrn  27159  lmiclbs  27175  hbtlem5  27200  itgocn  27237  f1otrspeq  27258  pm10.251  27423  pm11.63  27462  ax10ext  27474  iotain  27485  iotasbc  27487  stirlinglem13  27702  hirstL-ax3  27727  rexrsb  27814  raaan2  27820  2reurex  27826  2rmoswap  27829  2reu3  27833  eldmressn  27851  fnresfnco  27857  funressnfv  27859  afvpcfv0  27877  afvfv0bi  27883  afveu  27884  afvres  27903  tz6.12-afv  27904  afvco2  27907  aovvdm  27916  aovvfunressn  27918  aovrcl  27920  aovnuoveq  27922  aovvoveq  27923  aovovn0oveq  27925  aoprssdm  27933  ndmaovass  27937  ndmaovdistr  27938  nelprd  27943  otiunsndisj  27954  otiunsndisjX  27955  ssfz12  27976  elfzmlbp  27978  elfzelfzelfz  27981  2elfz3nn0  27984  ubmelfzo  27986  ubmelm1fzo  27987  fzo1fzo0n0  27988  hashfzdm  27997  euhash1  27998  iswrd0i  27999  swrdnd  28001  addlenrevswrd  28004  swrd0swrd  28009  swrdswrdlem  28010  swrdswrd  28011  swrd0swrdid  28012  swrdccatin1  28016  swrdccatin2  28018  swrdccatin12lem1  28019  swrdccatin12lem3a  28021  swrdccatin12lem3b  28022  swrdccatin12lem3c  28023  swrdccatin12lem3  28024  swrdccatin12lem4  28025  swrdccatin12  28026  swrdccatin12b  28027  swrdccatin12c  28028  swrdccat3  28029  swrdccat3a  28030  swrdccat3b  28031  uhgraedgrnv  28032  2wlkonot3v  28072  2spthonot3v  28073  2wlkonotv  28074  2spontn0vne  28084  frgra3vlem1  28104  frgra3vlem2  28105  3vfriswmgralem  28108  1to2vfriswmgra  28110  1to3vfriswmgra  28111  2pthfrgra  28115  3cyclfrgrarn1  28116  n4cyclfrgra  28122  vdgfrgragt2  28132  frgrancvvdeqlem1  28133  frgrancvvdeqlem3  28135  frgrancvvdeqlem7  28139  frgrancvvdeqlemA  28140  frgrancvvdeqlemB  28141  frgrancvvdeqlemC  28142  frgrancvvdeqlem9  28144  frgrawopreglem2  28148  frgrawopreglem3  28149  frgrawopreglem4  28150  frgrawopreglem5  28151  frgrawopreg1  28153  frgrawopreg2  28154  frgraregorufr0  28155  frgraregorufr  28156  frgraeu  28157  frg2wot1  28160  frg2woteqm  28162  2spotmdisj  28171  ifnmfalse  28220  bi123imp0  28293  2sb5nd  28358  uun132  28606  uun132p1  28607  uun2131p1  28613  a9e2eqVD  28728  2sb5ndVD  28731  2sb5ndALT  28754  bnj145  28800  bnj158  28802  bnj228  28808  bnj521  28810  bnj563  28817  bnj832  28832  bnj833  28833  bnj835  28834  bnj836  28835  bnj837  28836  bnj769  28837  bnj770  28838  bnj771  28839  bnj1098  28860  bnj1143  28867  bnj1232  28881  bnj1238  28884  bnj1254  28887  bnj1385  28910  bnj1533  28929  bnj110  28935  bnj98  28944  bnj517  28962  bnj518  28963  bnj535  28967  bnj543  28970  bnj544  28971  bnj546  28973  bnj570  28982  bnj605  28984  bnj590  28987  bnj594  28989  bnj600  28996  bnj906  29007  bnj916  29010  bnj944  29015  bnj953  29016  bnj970  29024  bnj998  29033  bnj1006  29036  bnj1018  29039  bnj1118  29059  bnj1128  29065  bnj1125  29067  bnj1145  29068  bnj1498  29136  exdistrfNEW7  29211  equviniNEW7  29231  equveliNEW7  29232  ax7w9AUX7  29360  opposet  29665  op0cl  29667  op1cl  29668  hlsuprexch  29863  hlhgt4  29870  atex  29888  dalemkehl  30105  dalempea  30108  dalemqea  30109  dalemrea  30110  dalemsea  30111  dalemtea  30112  dalemuea  30113  dalemyeo  30114  dalemzeo  30115  dalemclpjs  30116  dalemclqjt  30117  dalemclrju  30118  dalem-clpjq  30119  dalemceb  30120  dalemcnes  30132  dalempnes  30133  dalemqnet  30134  dalemswapyz  30138  dalemrot  30139  dalem5  30149  dalem-cly  30153  dalemccea  30165  dalemddea  30166  dalem-ddly  30168  dalemccnedd  30169  dalemclccjdd  30170  linepsubN  30234  pmapsub  30250  paddasslem9  30310  paddasslem10  30311  pclfinN  30382  pclcmpatN  30383  4atexlemk  30529  4atexlemw  30530  4atexlempw  30531  4atexlemq  30533  4atexlems  30534  4atexlemt  30535  4atexlemutvt  30536  4atexlempnq  30537  4atexlemnslpq  30538  4atexlemswapqr  30545  4atexlemnclw  30552  4atexlemcnd  30554  isltrn2N  30602  dochsnkrlem1  31952
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