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

Theorem syl5bi 217
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 12-Jan-1993.)
Hypotheses
Ref Expression
syl5bi.1
syl5bi.2
Assertion
Ref Expression
syl5bi

Proof of Theorem syl5bi
StepHypRef Expression
1 syl5bi.1 . . 3
21biimpi 194 . 2
3 syl5bi.2 . 2
42, 3syl5 32 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  3imtr4g  270  ancomsd  454  3jao  1289  ax12indn  2273  2euex  2366  2eu1  2376  eqneqall  2664  necon3bd  2669  necon2adOLD  2671  necon1adOLD  2674  pm2.61dne  2774  spcimgft  3185  rspc  3204  rspcimdv  3211  euind  3286  reuind  3303  sbciegft  3358  rspsbc  3417  ssexnelpss  3892  pwpw0  4178  sssn  4188  eqsn  4191  prel12  4207  prnebg  4212  pwsnALT  4244  intss1  4301  intmin  4306  uniintsn  4324  iinss  4381  disji2  4439  disjiun  4442  disjxiun  4449  disjss3  4451  trel3  4553  trin  4555  trintss  4561  eusvnfb  4648  reusv3  4660  copsexg  4737  copsexgOLD  4738  otiunsndisj  4758  po3nr  4819  fri  4846  wefrc  4878  wereu2  4881  onfr  4922  ord0eln0  4937  onmindif  4972  frsn  5075  ssrelrel  5108  relop  5158  iss  5326  restidsing  5335  poirr2  5396  xpcan  5448  xpcan2  5449  sossfld  5459  funopg  5625  funssres  5633  funun  5635  fv3  5884  fvmptt  5971  iinpreima  6017  suppssOLD  6020  fvn0ssdmfun  6022  dff3  6044  dff4  6045  fmptsng  6092  fmptsnd  6093  fnprb  6129  fnprOLD  6130  fvclss  6154  isomin  6233  isofrlem  6236  weniso  6250  oprabid  6323  ssorduni  6621  onmindif2  6647  limuni3  6687  tfis2f  6690  tfinds  6694  tfinds2  6698  tfinds3  6699  funcnvuni  6753  f1oweALT  6784  f1o2ndf1  6908  poxp  6912  soxp  6913  fnse  6917  suppimacnv  6929  mpt2xopynvov0g  6961  reldmtpos  6982  rntpos  6987  onfununi  7031  smoiun  7051  tfrlem1  7064  tfr3  7087  frsucmptn  7123  tz7.49  7129  oaordi  7214  oawordeulem  7222  omeulem1  7250  oeordi  7255  oelimcl  7268  nnaordi  7286  nneob  7320  omsmolem  7321  erdisj  7378  qsss  7391  uniinqs  7410  map0g  7478  resixpfo  7527  ixpsnf1o  7529  xpdom3  7635  mapdom3  7709  phplem4  7719  php3  7723  unxpdomlem3  7746  ssfi  7760  findcard2  7780  findcard3  7783  frfi  7785  isfiniteg  7800  xpfi  7811  fiint  7817  finsschain  7847  dffi2  7903  marypha1lem  7913  marypha2  7919  supmo  7932  suplub2  7941  ordiso2  7961  ordtypelem7  7970  ordtypelem8  7971  brwdom2  8020  unxpwdom2  8035  ixpiunwdom  8038  elirrv  8044  suc11reg  8057  noinfep  8097  cantnfle  8111  cantnflem1  8129  cantnf  8133  cantnfleOLD  8141  cantnflem1OLD  8152  cantnfOLD  8155  trcl  8180  epfrs  8183  rankpwi  8262  rankunb  8289  rankuni2b  8292  rankxplim3  8320  cplem1  8328  karden  8334  carddom2  8379  fseqenlem2  8427  ac10ct  8436  acni2  8448  acndom  8453  infpwfien  8464  alephordi  8476  alephord  8477  iunfictbso  8516  aceq3lem  8522  dfac5  8530  dfac2  8532  dfac12lem3  8546  dfac12r  8547  cdainflem  8592  cdainf  8593  cfub  8650  cfeq0  8657  coflim  8662  cfslb2n  8669  cofsmo  8670  coftr  8674  infpssr  8709  fin23lem7  8717  fin23lem11  8718  fin23lem21  8740  isf32lem2  8755  isf34lem4  8778  isfin1-2  8786  isfin1-3  8787  fin1a2lem9  8809  fin1a2lem11  8811  fin1a2lem12  8812  fin1a2lem13  8813  domtriomlem  8843  axdc3lem2  8852  axcclem  8858  ac6c4  8882  zorn2lem4  8900  zorn2lem5  8901  zorn2lem7  8903  ttukeylem5  8914  ttukeyg  8918  brdom6disj  8931  fnrndomg  8934  iunfo  8935  iundom2g  8936  ficard  8961  konigthlem  8964  alephval2  8968  pwcfsdom  8979  fpwwe2lem9  9037  fpwwe2lem11  9039  fpwwe2lem12  9040  fpwwe2lem13  9041  pwfseqlem3  9059  gchpwdom  9069  winalim2  9095  gchina  9098  wunex2  9137  tskr1om2  9167  tskxpss  9171  inar1  9174  tskuni  9182  gruun  9205  grudomon  9216  grur1  9219  ltmpi  9303  ltexprlem2  9436  ltexprlem6  9440  reclem2pr  9447  reclem3pr  9448  reclem4pr  9449  suplem1pr  9451  mulgt0sr  9503  supsrlem  9509  axrrecex  9561  axpre-sup  9567  ltlen  9707  mulge0b  10437  supmul1  10533  supmullem1  10534  supmullem2  10535  supmul  10536  infmrcl  10547  cju  10557  nnsub  10599  0mnnnnn0  10853  un0addcl  10854  un0mulcl  10855  nn0sub  10871  nn0n0n1ge2b  10885  peano5uzi  10976  eluzuzle  11118  negn0  11197  zsupss  11200  qbtwnre  11427  xrsupexmnf  11525  xrinfmexpnf  11526  xrsupsslem  11527  xrinfmsslem  11528  xrub  11532  supxrun  11536  xrinfm0  11557  ixxdisj  11573  icodisj  11674  difreicc  11681  uzsubsubfz  11736  elfzmlbp  11815  fzofzim  11869  elfznelfzo  11915  injresinj  11926  flval3  11951  modirr  12057  ssnn0fi  12094  seqf1o  12148  expcl2lem  12178  expnegz  12200  expaddz  12210  expmulz  12212  facwordi  12367  faclbnd4lem4  12374  bccl  12400  hashnfinnn0  12432  hashgt12el  12481  hashgt12el2  12482  hashfun  12495  hashbclem  12501  hashbc  12502  hashfacen  12503  hashf1lem1  12504  hashf1  12506  hash2pwpr  12519  brfi1uzind  12532  wrdind  12702  wrd2ind  12703  reuccats1  12706  swrdccatin1  12708  swrdccatin2  12712  swrdccat3  12717  swrdccat3blem  12720  cshw1  12790  cshwcsh2id  12796  wwlktovfo  12896  sqrlem1  13076  sqrlem6  13081  rexanre  13179  cau3lem  13187  2clim  13395  summo  13539  fsum2dlem  13585  fsumiun  13635  prodmo  13743  fprod2dlem  13784  rpnnen2  13959  odd2np1lem  14045  bitsfzo  14085  sadcaddlem  14107  gcd0id  14161  algcvgblem  14206  prmdvdsexpr  14257  prmfac1  14259  qnumdencl  14272  hashdvds  14305  pcneg  14397  prmpwdvds  14422  prmreclem2  14435  4sqlem12  14474  vdwlem6  14504  vdwlem10  14508  vdwlem13  14511  0ram  14538  ram0  14540  ramz  14543  ramcl  14547  cshwshashlem1  14580  prmlem0  14591  firest  14830  imasaddfnlem  14925  imasvscafn  14934  mremre  15001  drsdirfi  15567  pospo  15603  joinfval  15631  meetfval  15645  lubun  15753  odupos  15765  acsfiindd  15807  psss  15844  mnd1id  15963  symgfix2  16441  f1omvdco2  16473  symggen  16495  odcau  16624  pgpfi  16625  sylow2blem3  16642  sylow3lem2  16648  lsmmod  16693  efgsfo  16757  frgpuptinv  16789  frgpnabllem1  16877  cyggeninv  16886  lt6abl  16897  cyggex2  16899  gsumval3OLD  16908  gsumval3lem2  16910  gsumval3  16911  gsum2d2  17002  dmdprdd  17030  dprd2da  17091  pgpfac1lem5  17130  pgpfac  17135  srgbinomlem4  17194  dvdsrtr  17301  dvdsrmul1  17302  lss1d  17609  lspsolvlem  17788  lspsnat  17791  lbsextlem2  17805  lbsextlem3  17806  0ring  17918  01eq0ring  17920  0ring01eqbi  17921  rng1nfld  17926  domnmuln0  17947  abvn0b  17951  mvrf1  18081  mplcoe5lem  18130  opsrtoslem2  18149  cply1mul  18335  coe1fzgsumdlem  18343  gsummoncoe1  18346  pf1ind  18391  evl1gsumdlem  18392  xrsdsreclblem  18464  qsssubdrg  18477  prmirredlem  18523  prmirredlemOLD  18526  cygznlem3  18608  obslbs  18761  dsmmacl  18772  lindfrn  18856  lmiclbs  18872  lmisfree  18877  matecl  18927  mat1dimelbas  18973  scmateALT  19014  mdetdiaglem  19100  mdet0  19108  mdetunilem9  19122  gsummatr01  19161  cpmatmcllem  19219  m2cpminvid2lem  19255  pmatcollpw3fi1lem2  19288  chfacfscmul0  19359  chfacfpmmul0  19363  cayhamlem3  19388  unitgOLD  19469  tgcl  19471  tgidm  19482  indistopon  19502  fctop  19505  cctop  19507  ppttop  19508  pptbas  19509  epttop  19510  opnnei  19621  neiptopnei  19633  tgrest  19660  restntr  19683  perfopn  19686  ordtrest2lem  19704  isreg2  19878  lmmo  19881  ordthauslem  19884  cmpsublem  19899  cmpsub  19900  cmpcld  19902  hauscmplem  19906  bwthOLD  19911  iunconlem  19928  uncon  19930  2ndcrest  19955  2ndcctbss  19956  2ndcdisj  19957  dis2ndc  19961  locfincmp  20027  comppfsc  20033  txbas  20068  ptbasin  20078  ptbasfi  20082  txcls  20105  txbasval  20107  ptpjopn  20113  ptclsg  20116  dfac14lem  20118  xkoccn  20120  txcnp  20121  txindis  20135  txdis1cn  20136  tx1stc  20151  tx2ndc  20152  txkgen  20153  xkoco1cn  20158  xkoco2cn  20159  xkococn  20161  xkoinjcn  20188  txcon  20190  fbfinnfr  20342  opnfbas  20343  filtop  20356  isfild  20359  fbunfip  20370  filcon  20384  fbasrn  20385  filuni  20386  isufil2  20409  filssufilg  20412  ufileu  20420  filufint  20421  rnelfmlem  20453  rnelfm  20454  fmfnfmlem2  20456  fmfnfmlem4  20458  fmfnfm  20459  hausflimi  20481  hauspwpwf1  20488  flffbas  20496  flftg  20497  alexsublem  20544  alexsubALTlem1  20547  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  alexsubALT  20551  ptcmplem3  20554  cldsubg  20609  qustgpopn  20618  tgptsmscld  20653  tsmsxplem1  20655  ustfilxp  20715  imasdsf1olem  20876  bldisj  20901  xbln0  20917  prdsxmslem2  21032  xrsblre  21316  icccmplem2  21328  reconn  21333  opnreen  21336  xrge0tsms  21339  metdsre  21357  iccpnfcnv  21444  cnheiborlem  21454  phtpc01  21496  pi1blem  21539  tchcph  21680  cfilfcls  21713  iscau4  21718  bcthlem5  21767  bcth3  21770  hlhil  21858  ovolctb  21901  ovoliunlem2  21914  ovoliunnul  21918  ovolicc2  21933  volfiniun  21957  iundisj  21958  dyadmax  22007  dyadmbllem  22008  vitalilem2  22018  ismbfd  22047  mbfimaopnlem  22062  itg11  22098  i1faddlem  22100  mbfi1fseqlem4  22125  bddmulibl  22245  limciun  22298  perfdvf  22307  rolle  22391  dvivthlem1  22409  dvne0  22412  lhop1  22415  lhop2  22416  itgsubst  22450  dvdsq1p  22561  fta1g  22568  dgrco  22672  plydivex  22693  fta1  22704  ulmcaulem  22789  abelthlem2  22827  pilem2  22847  cxpmul2z  23072  cxpcn3lem  23121  xrlimcnp  23298  jensen  23318  wilthlem2  23343  wilthlem3  23344  muval2  23408  sqf11  23413  ppiublem1  23477  fsumvma  23488  lgsdir2lem2  23599  lgsdir2lem5  23602  dchrisum0fno1  23696  pntlem3  23794  pntleml  23796  ostthlem1  23812  ostth2lem2  23819  colinearalg  24213  axcontlem2  24268  axcontlem8  24274  usgrares1  24410  nbgraf1olem5  24445  cusgrarn  24459  nbcusgra  24463  uvtxnbgra  24493  wlkcpr  24529  3v3e3cycl2  24664  usg2wlkeq  24708  wlkiswwlksur  24719  clwlkswlks  24758  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem1  24787  clwwlkf1  24796  erclwwlktr  24815  erclwwlkntr  24827  hashecclwwlkn1  24834  usghashecclwwlk  24835  wlklenvclwlk  24839  clwlkfoclwwlk  24845  vdusgra0nedg  24908  nbhashuvtx  24916  usgravd0nedg  24918  usgravd00  24919  rusgranumwlklem1  24949  3cyclfrgrarn1  25012  frgranbnb  25020  frgrancvvdeqlem3  25032  frgrancvvdeqlem4  25033  frgrancvvdeqlemC  25039  frgrawopreglem3  25046  frgrawopreglem5  25048  frgrawopreg2  25051  2spotiundisj  25062  2spotmdisj  25068  extwwlkfablem2  25078  numclwwlkun  25079  numclwwlkovf2ex  25086  numclwlk1lem2f1  25094  gxnn0neg  25265  gxnn0suc  25266  lnon0  25713  shmodsi  26307  shlub  26332  spanunsni  26497  h1datomi  26499  stm1ri  27163  stadd3i  27167  mdsl1i  27240  cvmdi  27243  superpos  27273  chjatom  27276  chirredi  27313  atcvat4i  27316  sumdmdii  27334  sumdmdlem  27337  cdj3lem2a  27355  cdj3lem3a  27358  cdj3i  27360  disji2f  27438  disjif2  27442  iundisjf  27448  rnmpt2ss  27515  xrge0infss  27580  iundisjfi  27601  nn0min  27611  xrge0tsmsd  27775  cnre2csqima  27893  ordtrest2NEWlem  27904  xrge0iifcnv  27915  lmxrge0  27934  measdivcstOLD  28195  dya2iocuni  28254  eulerpartlems  28299  derangenlem  28615  erdszelem9  28643  pconcon  28676  iccllyscon  28695  cvmsval  28711  cvmscld  28718  cvmsss2  28719  cvmopnlem  28723  cvmfolem  28724  cvmliftmolem2  28727  cvmlift2lem10  28757  cvmlift2lem12  28759  cvmlift3lem5  28768  cvmlift3lem8  28771  msubvrs  28920  mthmblem  28940  rtrclreclem.trans  29069  dfrtrcl2  29071  untsucf  29082  3orel1  29087  3orel2  29088  3orel3  29089  nepss  29095  dfon2lem5  29219  dfon2lem6  29220  dfon2lem7  29221  dfon2lem8  29222  rdgprc  29227  wfi  29287  wfis2fg  29291  trpredtr  29313  dftrpred3g  29316  trpredrec  29321  frmin  29322  frind  29323  frins2fg  29327  wfrlem14  29356  wfrlem15  29357  wsuclem  29381  frrlem5e  29395  nodenselem4  29444  nodenselem8  29448  nocvxmin  29451  nofulllem5  29466  funpartfun  29593  altopth1  29615  altopth2  29616  colineardim1  29711  lineext  29726  btwnconn1lem14  29750  brsegle  29758  hilbert1.2  29805  bpolycl  29814  arg-ax  29881  ordtoplem  29900  onsuct0  29906  fin2so  30040  supaddc  30041  supadd  30042  mblfinlem1  30051  mblfinlem4  30054  ovoliunnfl  30056  itg2addnclem  30066  itg2addnclem2  30067  areacirc  30112  trer  30134  elicc3  30135  finminlem  30136  fneint  30166  fnessref  30175  refssfne  30176  neibastop1  30177  neibastop2lem  30178  neibastop2  30179  fnemeet2  30185  fnejoin2  30187  tailfb  30195  unirep  30203  filbcmb  30231  fzadd2  30234  sdclem1  30236  fdc  30238  nninfnub  30244  isbnd2  30279  ssbnd  30284  prdsbnd2  30291  cntotbnd  30292  heibor1lem  30305  heiborlem1  30307  heiborlem4  30310  heiborlem6  30312  0idl  30422  intidl  30426  unichnidl  30428  keridl  30429  prnc  30464  ceqsex3OLD  30601  prtlem17  30617  prter2  30622  eldioph2b  30696  eldiophss  30708  diophren  30747  ctbnfien  30752  rencldnfilem  30754  pellexlem3  30767  pellexlem5  30769  pellex  30771  pell14qrexpcl  30803  pellfundre  30817  pellfundge  30818  pellfundlb  30820  pellfundglb  30821  jm2.19lem4  30934  fnwe2lem2  30997  pwssplit4  31035  hbtlem5  31077  isprm7  31192  hirstL-ax3  32087  2reurex  32186  elnelall  32293  ralnralall  32294  otiunsndisjX  32301  subsubelfzo0  32338  usgra2pthspth  32351  usgvincvad  32404  usgvincvadALT  32407  usgedgvadf1lem2  32414  usgedgvadf1ALTlem2  32417  usgfis  32446  usgfisALT  32450  mgmpropd  32463  copisnmnd  32497  mgm2mgm  32551  tpres  32554  cicsym  32588  initoid  32611  termoid  32612  iszeroi  32615  ringrng  32685  c0snmgmhm  32720  ztprmneprm  32936  mndpsuppss  32964  lindslinindimp2lem4  33062  lindslinindsimp2  33064  lindsrng01  33069  snlindsntor  33072  ldepspr  33074  isldepslvec2  33086  onfrALT  33321  ax6e2ndeq  33332  snssiALT  33628  bnj849  33983  bnj1118  34040  bj-gl4lem  34183  bj-sngltag  34541  bj-bary1lem1  34680  lsatn0  34724  lsatcmp  34728  lssat  34741  lfl1  34795  lshpsmreu  34834  lkrin  34889  glbconxN  35102  cvrat4  35167  paddasslem17  35560  pmodlem2  35571  dalawlem14  35608  pclclN  35615  pclfinN  35624  pclfinclN  35674  poml4N  35677  osumcllem8N  35687  pexmidlem5N  35698  cdleme32a  36167  cdlemg33b0  36427  tendoeq2  36500  diaelrnN  36772  dihmeetlem1N  37017  dihglblem5apreN  37018  dihglblem2N  37021  dochvalr  37084  dochkrshp  37113  lcfl6  37227  lcfrvalsnN  37268  mapdordlem2  37364  mapdh8b  37507  mapdh9a  37517  hdmap14lem13  37610
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator