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

Theorem sylbi 187
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 186 . 2  |-  ( ph  ->  ps )
3 sylbi.2 . 2  |-  ( ps 
->  ch )
42, 3syl 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  bi2  189  3imtr4i  257  sylnbi  297  imp  418  an12s  776  an32s  779  an4s  799  oibabs  851  3simpb  953  3simpc  954  3imp  1145  3com12  1155  3com13  1156  syl3anb  1225  19.33b  1595  exintrbi  1600  spimfw  1627  nfr  1741  a6e  1755  nfnd  1760  equs5e  1829  exdistrf  1911  equvini  1927  equveli  1928  ax10-16  2129  euex  2166  eumo0  2167  mopick  2205  2euex  2215  2mo  2221  2eu3  2225  exists2  2233  eqcoms  2286  eleq2s  2375  nfcr  2411  necon3bi  2487  necon1ai  2488  necon2ai  2491  pm2.61ne  2521  pm2.61ine  2522  rexex  2602  rsp  2603  ralim  2614  r19.36av  2688  r19.37  2689  r19.44av  2696  r19.45av  2697  gencl  2816  gencbvex  2830  vtoclgf  2842  pm13.183  2908  mo2icl  2944  mob2  2945  reu3  2955  rmoim  2964  2reuswap  2967  sbcex  3000  ra5  3075  sseq1  3199  unineq  3419  dfrab3ss  3446  reldisj  3498  disjel  3501  pssdif  3516  difin0ss  3520  uneqdifeq  3542  r19.2z  3543  r19.3rz  3545  r19.3rzv  3547  ralidm  3557  ifnefalse  3573  ifbi  3582  nelpri  3661  prprc1  3736  pwpw0  3763  ssunsn2  3773  snsssn  3781  preqr2  3787  preq12b  3788  opthpr  3790  pwsnALT  3822  intmin4  3891  dfiin2g  3936  iinss2  3954  invdisj  4012  disjiun  4013  trel  4120  trss  4122  trint0  4130  axrep5  4136  zfrep4  4139  ssex  4158  intex  4167  intnex  4168  intabs  4172  abssexg  4195  axpr  4213  rext  4222  unipw  4224  moabex  4232  nnullss  4235  exss  4236  copsexg  4252  pwssun  4299  epelg  4306  solin  4337  elsuci  4458  sucprc  4467  ordsssuc2  4481  ordssun  4492  ordequn  4493  onun2i  4508  reusv2lem1  4535  reusv2lem4  4538  reusv3  4542  reusv5OLD  4544  elpwunsn  4568  onmindif2  4603  suceloni  4604  ordpwsuc  4606  onsucmin  4612  ordsucelsuc  4613  ordsucun  4616  unon  4622  ordunisuc  4623  0elsuc  4626  onuninsuci  4631  orduninsuc  4634  limsuc  4640  limuni3  4643  tfi  4644  tfindsg  4651  limomss  4661  limom  4671  find  4681  findsg  4683  0nelelxp  4718  opelxp  4719  elvvuni  4750  posn  4758  frsn  4760  optocl  4764  xpsspwOLD  4798  ralxpf  4830  relop  4834  breldm  4883  elreldm  4903  dmrnssfld  4938  dmcosseq  4946  resabs1  4984  resima2  4988  relimasn  5036  issref  5056  asymref  5059  asymref2  5060  xpidtr  5065  trin2  5066  poirr2  5067  xpnz  5099  xp11  5111  xpcan  5112  xpcan2  5113  cnveqb  5129  dfco2a  5173  cores2  5185  coi2  5189  relcnvtr  5192  relresfld  5199  unixp0  5206  unixpid  5207  relcnvexb  5210  iotauni  5231  iota1  5233  iota4  5237  dffun8  5281  funcnvsn  5297  imadif  5327  fcoi1  5415  fcoi2  5416  f1ocnv  5485  f1ocnvb  5486  fun11iun  5493  ffoss  5505  f1o00  5508  fo00  5509  nfunsn  5558  fnrnfv  5569  ssimaex  5584  dffv2  5592  fvmptss  5609  fvmptss2  5619  fvimacnv  5640  unpreima  5651  respreima  5654  dffo4  5676  exfo  5678  funressn  5706  fvpr1  5722  fvpr2  5723  fvtp1  5724  fconst5  5731  eufnfv  5752  elunirnALT  5779  isores1  5831  f1oweALT  5851  oprabid  5882  oprssdm  6002  1stval2  6137  2ndval2  6138  fo1stres  6143  fo2ndres  6144  1st2val  6145  2nd2val  6146  xp1st  6149  xp2nd  6150  unielxp  6158  releldm2  6170  cnvf1o  6217  frxp  6225  poxp  6227  reldmtpos  6242  dftpos4  6253  tpostpos  6254  tpostpos2  6255  sorpssun  6284  sorpssin  6285  sorpssuni  6286  sorpssint  6287  opabiota  6293  riotauni  6311  riotacl2  6318  riota1  6323  riota1a  6324  snriota  6335  eusvobj2  6337  iunon  6355  iinon  6357  smoel  6377  tfrlem4  6395  tfrlem5  6396  tfrlem7  6399  tfrlem8  6400  tfrlem9  6401  tfr2b  6412  rdgsucg  6436  frsuc  6449  tz7.48lem  6453  tz7.48-1  6455  tz7.49  6457  abianfp  6471  oesuclem  6524  oaord  6545  nnaord  6617  nneob  6650  ecexr  6665  swoord1  6689  swoord2  6690  0er  6695  ecdmn0  6702  mapprc  6776  mapsnconst  6813  ixpprc  6837  ixpf  6838  ixpn0  6848  ixp0  6849  undifixp  6852  mptelixpg  6853  boxriin  6858  idssen  6906  ener  6908  en0  6924  en1  6928  en1b  6929  2dom  6933  snfi  6941  xpsnen  6946  sbthlem1  6971  sbthlem10  6980  domnsym  6987  2pwuninel  7016  ssenen  7035  php  7045  php3  7047  ominf  7075  isinf  7076  pssnn  7081  ssfi  7083  enp1i  7093  findcard  7097  findcard2  7098  findcard3  7100  difinf  7127  infcntss  7130  fiint  7133  pwfi  7151  elfiun  7183  card2on  7268  brwdomn0  7283  unwdomg  7298  unxpwdom2  7302  ixpiunwdom  7305  sucprcreg  7313  inf0  7322  inf3lem1  7329  infeq5i  7337  infeq5  7338  dfom3  7348  trcl  7410  epfrs  7413  setind2  7420  tz9.12lem3  7461  rankwflemb  7465  rankf  7466  rankidb  7472  snwf  7481  uniwf  7491  rankpwi  7495  rankunb  7522  rankuni2b  7525  rankuni  7535  rankxpsuc  7552  tcrank  7554  scottex  7555  scott0  7556  bnd2  7563  karden  7565  finnum  7581  carduni  7614  cardiun  7615  dif1card  7638  infxpenlem  7641  fseqenlem2  7652  acnrcl  7669  acndom  7678  acnnum  7679  alephfp  7735  iunfictbso  7741  dfac4  7749  dfac5lem4  7753  dfac5  7755  dfac2  7757  dfac9  7762  dfac12r  7772  kmlem2  7777  kmlem4  7779  kmlem12  7787  kmlem13  7788  ackbij2  7869  cardcf  7878  cfeq0  7882  cfsuc  7883  alephsing  7902  fin4en1  7935  enfin2i  7947  fin23lem16  7961  fin23lem21  7965  fin23lem29  7967  fin23lem30  7968  fin23lem40  7977  isfin32i  7991  isfin1-2  8011  fin34  8016  fin45  8018  fin17  8020  fin67  8021  isfin7-2  8022  fin1a2lem7  8032  fin1a2lem10  8035  fin1a2lem12  8037  itunitc  8047  axcc4dom  8067  dcomex  8073  axdc3lem4  8079  axdc4lem  8081  axcclem  8083  ac6c4  8108  ac6sf  8116  ac6s4  8117  zorn2lem6  8128  zorn2lem7  8129  zorng  8131  zornn0g  8132  ttukeylem6  8141  ttukey2g  8143  brdom5  8154  brdom4  8155  unirnfdomd  8189  alephval2  8194  alephadd  8199  alephmul  8200  alephsuc3  8202  alephexp2  8203  alephreg  8204  pwcfsdom  8205  cfpwsdom  8206  fpwwe2lem8  8259  gchinf  8279  pwfseq  8286  winaon  8310  winacard  8314  winainf  8316  tsk0  8385  tskcard  8403  r1tskina  8404  gruima  8424  intgru  8436  ingru  8437  gruina  8440  axgroth6  8450  grothomex  8451  indpi  8531  nqereu  8553  nqerf  8554  ordpipq  8566  prn0  8613  prpssnq  8614  nqpr  8638  ltexprlem4  8663  reclem2pr  8672  mulcmpblnr  8696  recexsrlem  8725  map2psrpr  8732  supsr  8734  axpre-sup  8791  1re  8837  renfdisj  8885  ltxrlt  8893  lemul1a  9610  ltdiv2OLD  9642  sup3  9711  supmul1  9719  supmullem1  9720  supmul  9722  peano2nn  9758  nn0ge0  9991  elnnnn0b  10008  nn0sub  10014  znegcl  10055  zeo  10097  nn0ind  10108  nn0ind-raph  10112  uzn0  10243  eluzaddi  10254  eluzsubi  10255  uznn0sub  10259  uznnssnn  10266  uz2m1nn  10292  uz2mulcl  10295  indstr2  10296  qmulz  10319  qre  10321  qnegcl  10333  qreccl  10336  rphalflt  10380  xrltnr  10462  xnegcl  10540  xnegneg  10541  xltnegi  10543  xnegid  10563  xaddid1  10566  xmulid1  10599  xrsupsslem  10625  xrinfmsslem  10626  xrsupss  10627  xrinfmss  10628  elioore  10686  ioorebas  10745  elfzuz2  10801  fzn0  10809  fzdisj  10817  fzon0  10891  fzoss1  10896  fzind2  10923  om2uzrani  11015  uzrdgfni  11021  fzfi  11034  expcl2lem  11115  crreczi  11226  nn0opthlem2  11284  nn0opthi  11285  facp1  11293  facnn2  11297  faclbnd3  11305  faclbnd4lem1  11306  faclbnd4lem3  11308  bcn1  11325  hashfun  11389  hashf1lem2  11394  iswrdi  11417  wrdf  11419  swrd00  11451  swrdcl  11452  rexanuz  11829  fclim  12027  climmo  12031  rlimdiv  12119  caurcvg2  12150  fsum2dlem  12233  fsumcom2  12237  arisum  12318  arisum2  12319  ef01bndlem  12464  sin01gt0  12470  cos01gt0  12471  sin02gt0  12472  xpnnenOLD  12488  odd2np1  12587  divalglem1  12593  divalglem6  12597  ndvdsadd  12607  gcdaddmlem  12707  mulgcd  12725  algcvgblem  12747  algfx  12750  prmind2  12769  maxprmfct  12792  dfphi2  12842  pythagtriplem2  12870  pcz  12933  prmunb  12961  prmreclem3  12965  4sqlem4  12999  4sqlem19  13010  ramz  13072  firest  13337  imasaddfnlem  13430  xpsfrnel2  13467  mreiincl  13498  mreunirn  13503  mremre  13506  fnmrc  13509  mrcfval  13510  ismon2  13637  isepi2  13644  sscpwex  13692  funcres2b  13771  funcpropd  13774  funcres2c  13775  isfull  13784  isfth  13788  homa1  13869  homahom2  13870  cnvpsb  14322  spwmo  14335  laspwcl  14343  lanfwcl  14344  gsumval2  14460  subgint  14641  giclcl  14736  gicrcl  14737  gicsym  14738  gicen  14741  gicsubgen  14742  cntzssv  14804  oppgsubm  14835  oppgsubg  14836  gexcl3  14898  sylow3lem6  14943  efgmnvl  15023  efgsf  15038  efgsrel  15043  efgs1b  15045  efgredlema  15049  efgredlemd  15053  efgrelexlema  15058  efgrelexlemb  15059  frgpnabllem1  15161  cygabl  15177  cyggex2  15183  giccyg  15186  dprdval  15238  dprdssv  15251  pgpfac1  15315  dvdsrval  15427  isunit  15439  drngmuleq0  15535  opprsubrg  15566  subrgint  15567  lmhmlem  15786  lmiclcl  15823  lmicrcl  15824  lmicsym  15825  lvecvscan  15864  lspsncv0  15899  abvn0b  16043  evlslem4  16245  cnsubdrglem  16422  prmirred  16448  zlmlmod  16477  frgpcyg  16527  thlle  16597  tgiun  16717  distop  16733  ssntr  16795  isclo2  16825  indiscld  16828  lecldbas  16949  pnfnei  16950  mnfnei  16951  lmrcl  16961  cmpsublem  17126  cmpsub  17127  hauscmplem  17133  iuncon  17154  2ndctop  17173  2ndcsb  17175  2ndcredom  17176  2ndc1stc  17177  2ndcdisj  17182  2ndcsep  17185  kgenuni  17234  kgenftop  17235  kgenss  17238  kgenidm  17242  iskgen3  17244  kgencn3  17253  txuni2  17260  dfac14  17312  txcn  17320  txindis  17328  kqtop  17436  kqt0  17437  hmeocnvb  17465  hmphref  17472  hmphsym  17473  hmphen  17476  haushmphlem  17478  cmphmph  17479  conhmph  17480  reghmph  17484  nrmhmph  17485  hmphdis  17487  hmphindis  17488  indishmph  17489  hmphen2  17490  ist1-5lem  17511  fbncp  17534  isfil2  17551  fbasfip  17563  fgcl  17573  filunirn  17577  cfinfil  17588  fiufl  17611  ufinffr  17624  isfcls  17704  alexsubALTlem2  17742  alexsubALTlem3  17743  tmdcn2  17772  xmetunirn  17902  lpbl  18049  blcld  18051  met1stc  18067  met2ndci  18068  dscmet  18095  qdensere  18279  blssioo  18301  xrtgioo  18312  divcn  18372  iimulcl  18435  iimulcn  18436  iccpnfcnv  18442  isphtpc  18492  phtpc01  18494  cmetcaulem  18714  bcthlem4  18749  elovolm  18834  ovolmge0  18836  ovolgelb  18839  ovolfi  18853  iunmbl  18910  iunmbl2  18914  ioombl1  18919  ioorcl2  18927  ioorf  18928  ioorinv2  18930  ioorinv  18931  ioorcl  18932  dyaddisj  18951  dyadmax  18953  opnmblALT  18958  vitali  18968  mbfid  18991  itg1addlem4  19054  itg2uba  19098  itg2splitlem  19103  limcdif  19226  ellimc2  19227  limcres  19236  limccnp  19241  dvexp2  19303  dvexp3  19325  mpfrcl  19402  pf1rcl  19432  pf1ind  19438  elply2  19578  plyssc  19582  elqaa  19702  aannenlem1  19708  aannenlem2  19709  aannenlem3  19710  aaliou2  19720  taylfval  19738  ulmscl  19758  pserdvlem2  19804  reeff1o  19823  sincosq1sgn  19866  sincosq2sgn  19867  sincosq3sgn  19868  sincosq4sgn  19869  sinq12gt0  19875  logfac  19954  dvloglem  19995  logf1o2  19997  logtayl  20007  cxpexp  20015  resqrcn  20089  reasinsin  20192  birthdaylem1  20246  harmonicbnd3  20301  sqff1o  20420  musum  20431  bpos1  20522  2sqlem2  20603  2sqlem10  20613  chebbnd1  20621  chtppilim  20624  chpo1ub  20629  dchrisum0lem2a  20666  rplogsum  20676  pnt2  20762  ostth  20788  grposn  20882  gxsuc  20939  ismgm  20987  isexid2  20992  ablomul  21022  rngo1cl  21096  nmobndseqi  21357  nmobndseqiOLD  21358  ipasslem5  21413  h2hcau  21559  hvsubeq0i  21642  hvmulcan  21651  hvmulcan2  21652  bcsiALT  21758  hhcms  21782  hlimf  21817  isch3  21821  hsn0elch  21827  hhssnv  21841  shintcli  21908  hsupcl  21918  hsupunss  21922  sshjcl  21934  shsleji  21949  shsidmi  21963  hsupval2  21988  sshjval2  21990  spanuni  22123  h1de2i  22132  spanunsni  22158  cmbr3i  22179  osumcor2i  22223  spansncvi  22231  5oalem7  22239  3oalem3  22243  pjss2i  22259  pjssmii  22260  mayete3i  22307  mayete3iOLD  22308  nmop0h  22571  riesz3i  22642  nmopcoi  22675  opsqrlem5  22724  pjnmopi  22728  pjorthcoi  22749  pjssdif1i  22755  dfpjop  22762  elpjch  22769  pjin2i  22773  pjclem1  22775  pjclem2  22776  pjclem4a  22778  pj3lem1  22786  strlem1  22830  strlem3  22833  strlem4  22834  strlem5  22835  stri  22837  hstrlem3  22841  hstrlem4  22842  hstrlem5  22843  hstri  22845  stcltr1i  22854  dmdbr5  22888  mdsl1i  22901  mdslmd1lem2  22906  atne0  22925  atom1d  22933  shatomici  22938  chrelat2i  22945  atssma  22958  chirredi  22974  cmmdi  22996  sumdmdi  23000  dmdbr4ati  23001  dmdbr5ati  23002  dmdbr6ati  23003  dmdbr7ati  23004  cdj3lem1  23014  ballotlem2  23047  ballotlemfmpn  23053  ballotlem7  23094  2reuswap2  23137  rexunirn  23140  iuninc  23158  fimacnvinrn  23199  unipreima  23209  xppreima  23211  rnmptss  23238  xrofsup  23255  fzssnn  23276  xrsmulgzz  23307  xrge0iifcnv  23315  xrge0iifiso  23317  xrge0iifhom  23319  logbcl  23399  esumc  23430  hasheuni  23453  ofcfval  23459  sigaclfu  23480  elmbfmvol2  23572  dya2iocct  23581  probun  23622  subfacval3  23720  erdszelem2  23723  kur14lem7  23743  kur14lem9  23745  rellyscon  23782  cvmliftlem15  23829  cvmlift2lem12  23845  iseupa  23881  eupath  23905  ghomgrpilem2  23993  untangtr  24060  dedekind  24082  dedekindle  24083  fz0n  24097  br8  24113  br6  24114  br4  24115  eldm3  24119  fununiq  24126  setinds  24134  setinds2f  24135  dfon2lem3  24141  dfon2lem7  24145  dfon2lem8  24146  rdgprc0  24150  dfrdg2  24152  elpredim  24176  prednn  24201  tfisg  24204  wfisg  24209  nnsinds  24217  nn0sinds  24218  trpredmintr  24234  trpredrec  24241  frmin  24242  frinsg  24245  soseq  24254  wfrlem2  24257  wfrlem3  24258  wfrlem4  24259  wfrlem9  24264  wfrlem11  24266  wfrlem12  24267  frrlem2  24282  frrlem3  24283  frrlem4  24284  frrlem5c  24287  frrlem5e  24289  frrlem11  24293  nofun  24303  nodmon  24304  norn  24305  sltval2  24310  sltsgn1  24315  sltsgn2  24316  sltintdifex  24317  sltres  24318  nofulllem5  24360  txpss3v  24418  pprodss4v  24424  fnimage  24468  imageval  24469  dfrdg4  24488  altopthsn  24495  altxpsspw  24511  axlowdimlem13  24582  axlowdim1  24587  axcontlem4  24595  linethru  24776  bpoly2  24792  bpoly3  24793  bpoly4  24794  rankeq1o  24801  waj-ax  24853  amosym1  24865  ordtoplem  24874  onsucconi  24876  onintopsscon  24879  onsuct0  24880  limsucncmpi  24884  ordcmp  24886  onint1  24888  dvreasin  24923  areacirclem2  24925  areacirclem5  24929  condisd  24943  copsexgb  24966  nxtor  24985  ltl4ev  24992  nopsthph  24995  splint  25048  domrngref  25060  unfinsef  25069  isunscov  25074  restidsing  25076  twsymr  25078  prj1b  25079  prj3  25080  imfstnrelc  25081  fixpb  25093  inttrp  25108  celsor  25111  eqfnung2  25118  domintrefc  25125  sssu  25141  repcpwti  25161  cbcpcp  25162  prl  25167  dstr  25171  oriso  25214  preoref22  25229  dupre2  25244  inposet  25278  supwval  25284  dfps2  25289  toplat  25290  dfdir2  25291  fsumprd  25329  com2i  25416  fldi  25427  vecval3b  25452  svs2  25487  basexre  25522  nsn  25530  dmhmph  25533  rnhmph  25534  intopcoaconlem3b  25538  intopcoaconlem3  25539  qusp  25542  usptop  25550  islimrs4  25582  bwt2  25592  cntrset  25602  supbrr  25636  claddrv  25647  claddrvr  25648  addcomv  25655  issubrv  25672  subclrvd  25674  clsmulcv  25682  fnmulcv  25684  distmlva  25688  distsava  25689  divclcvd  25694  divclrvd  25695  intrr  25699  intvconlem1  25703  hdrmp  25706  algi  25727  dedi  25737  cati  25755  imonclem  25813  propsrc  25868  tartarmap  25888  eltintpar  25899  inttaror  25900  carinttar  25902  fnctartar  25907  fnctartar2  25908  cmpmor  25975  lemindclsbu  25995  clscnc  26010  fnckle  26045  fnckleb  26046  pfsubkl  26047  pgapspf  26052  pgapspf2  26053  isig1a2  26063  isig22  26065  elhaltdp  26067  gltpntl  26072  gltpntl2  26073  lineval5a  26088  isconcl5a  26101  isconcl5ab  26102  isconcl6a  26103  isconcl6ab  26104  isibg2aa  26112  isib2g1a1  26116  isibg1a2  26117  isibg2a  26118  isibg1a3a  26122  isibg1spa  26123  isibg1a5a  26124  bsstr  26128  nbssntr  26129  pxysxy  26142  lppotoslem  26143  lppotos  26144  bsstrs  26146  nbssntrs  26147  pdiveql  26168  finminlem  26231  nn0prpwlem  26238  nn0prpw  26239  cldbnd  26244  dfcon2OLD  26253  fnemeet2  26316  fdc  26455  subspopn  26466  sstotbnd3  26500  totbndbnd  26513  heiborlem3  26537  heiborlem8  26542  exidcl  26566  riscer  26619  divrngidl  26653  smprngopr  26677  prtlem9  26732  prtlem16  26737  prtlem14  26742  fndifnfp  26756  cmpfiiin  26772  ismrcd1  26773  isnacs3  26785  fzsplit1nn0  26833  eldiophss  26854  2nn0ind  27030  jm2.23  27089  expdiophlem1  27114  expdioph  27116  setindtrs  27118  dfac11  27160  lnmlmic  27186  gicabl  27263  isnumbasgrplem2  27269  dfacbasgrp  27273  lindfrn  27291  lmiclbs  27307  hbtlem5  27332  itgocn  27369  f1otrspeq  27390  pm10.251  27555  pm11.63  27594  ax10ext  27606  iotain  27617  iotasbc  27619  stoweidlem2  27751  stoweidlem57  27806  hirstL-ax3  27860  rexrsb  27947  raaan2  27953  2reurex  27959  2rmoswap  27962  2reu3  27966  eldmressn  27982  fvfundmfvn0  27986  fnresfnco  27989  funressnfv  27991  afvpcfv0  28009  afvfv0bi  28015  afvres  28034  tz6.12-afv  28035  afvco2  28037  aovvdm  28045  aovvfunressn  28047  aovrcl  28049  aovnuoveq  28051  aovvoveq  28052  aovovn0oveq  28054  aoprssdm  28062  ndmaovass  28066  ndmaovdistr  28067  diftpsneq  28070  tpprceq3  28072  prneimg  28073  mpt2xopxnop0  28081  elprchashprn2  28088  usgraedgprv  28122  usgraedgrnv  28123  usgra1v  28126  usgraexmpl  28133  nbusgra  28143  nbgra0nb  28144  nbgranself  28149  nbgrassovt  28150  nbgranself2  28151  cusgra1v  28157  cusgra2v  28158  nbcusgra  28159  cusgrauvtx  28168  frgra2v  28177  frgra3vlem1  28178  frgra3vlem2  28179  3vfriswmgralem  28182  1to2vfriswmgra  28184  1to3vfriswmgra  28185  ifnmfalse  28233  2sb5nd  28326  uun132  28560  uun132p1  28561  uun2131p1  28567  a9e2eqVD  28683  2sb5ndVD  28686  2sb5ndALT  28709  bnj145  28755  bnj158  28757  bnj228  28763  bnj521  28765  bnj563  28772  bnj832  28787  bnj833  28788  bnj835  28789  bnj836  28790  bnj837  28791  bnj769  28792  bnj770  28793  bnj771  28794  bnj1098  28815  bnj1143  28822  bnj1232  28836  bnj1238  28839  bnj1254  28842  bnj1385  28865  bnj1533  28884  bnj110  28890  bnj98  28899  bnj517  28917  bnj518  28918  bnj535  28922  bnj543  28925  bnj544  28926  bnj546  28928  bnj570  28937  bnj605  28939  bnj590  28942  bnj594  28944  bnj600  28951  bnj906  28962  bnj916  28965  bnj944  28970  bnj953  28971  bnj970  28979  bnj998  28988  bnj1006  28991  bnj1018  28994  bnj1118  29014  bnj1128  29020  bnj1125  29022  bnj1145  29023  bnj1398  29064  bnj1498  29091  ax12-3  29104  ax12conj2  29108  a12stdy2-x12  29112  a12stdy2  29127  a12lem2  29131  ax9lem11  29150  opposet  29372  op0cl  29374  op1cl  29375  hlsuprexch  29570  hlhgt4  29577  atex  29595  dalemkehl  29812  dalempea  29815  dalemqea  29816  dalemrea  29817  dalemsea  29818  dalemtea  29819  dalemuea  29820  dalemyeo  29821  dalemzeo  29822  dalemclpjs  29823  dalemclqjt  29824  dalemclrju  29825  dalem-clpjq  29826  dalemceb  29827  dalemcnes  29839  dalempnes  29840  dalemqnet  29841  dalemswapyz  29845  dalemrot  29846  dalem5  29856  dalem-cly  29860  dalemccea  29872  dalemddea  29873  dalem-ddly  29875  dalemccnedd  29876  dalemclccjdd  29877  linepsubN  29941  pmapsub  29957  paddasslem9  30017  paddasslem10  30018  pclfinN  30089  pclcmpatN  30090  4atexlemk  30236  4atexlemw  30237  4atexlempw  30238  4atexlemq  30240  4atexlems  30241  4atexlemt  30242  4atexlemutvt  30243  4atexlempnq  30244  4atexlemnslpq  30245  4atexlemswapqr  30252  4atexlemnclw  30259  4atexlemcnd  30261  isltrn2N  30309  dochsnkrlem1  31659
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