Theorem sylbi 121

Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 3-Jan-1993.)

Hypotheses

Ref	Expression
sylbi.1	⊢ (𝜑 ↔ 𝜓)
sylbi.2	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
sylbi	⊢ (𝜑 → 𝜒)

Proof of Theorem sylbi

Step	Hyp	Ref	Expression
1		sylbi.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 120	. 2 ⊢ (𝜑 → 𝜓)
3		sylbi.2	. 2 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylbb  123  sylbb2  138  3imtr4i  201  simplbiim  387  mpan10  474  an12s  567  an32s  570  an4s  592  sylnbi  684  dcim  848  notnotrdc  850  condcOLD  861  pm2.61ddc  868  pm5.18dc  890  pm2.25dc  900  pm2.85dc  912  pm5.12dc  917  pm5.14dc  918  pm5.55dc  920  peircedc  921  pm5.54dc  925  dcand  940  dcor  943  pm5.62dc  953  pm5.63dc  954  pm4.83dc  959  ifp2  988  ifpor  995  1fpid3  1002  3simpb  1021  3simpc  1022  3imp  1219  3com12  1233  3com13  1234  syl3anb  1316  xoranor  1421  xorbin  1428  xordc1  1437  biassdc  1439  nfr  1566  nfand  1616  19.21t  1630  19.30dc  1675  exintrbi  1681  19.9t  1690  nfnt  1703  equveli  1806  exdistrfor  1847  sbcof2  1857  sbidm  1898  sbi1v  1939  sbalyz  2051  sbal1yz  2053  nfsb4t  2066  euex  2108  eumo0  2109  mor  2121  exmodc  2129  mo3h  2132  mopick  2157  moexexdc  2163  euexex  2164  2euex  2166  exists2  2176  eqcoms  2233  eleq2s  2325  nfcr  2365  necon3ai  2450  rexnalim  2520  dfrex2dc  2522  rexex  2577  rsp  2578  ralim  2590  rexim  2625  r19.32r  2678  r19.44av  2691  r19.45av  2692  gencl  2834  gencbvex  2849  gencbval  2851  vtoclgf  2861  vtoclg1f  2862  pm13.183  2943  elrabi  2958  eueq2dc  2978  eueq3dc  2979  mob2  2985  euxfr2dc  2990  reu3  2995  rmoim  3006  2rmorex  3011  sbcex  3039  sbcbi2  3081  ra5  3120  sseq1  3249  difdif  3331  dfss4st  3439  difindiss  3460  undif3ss  3467  dfrab3ss  3484  abvor0dc  3517  reldisj  3545  disjel  3548  inssdif0im  3561  uneqdifeqim  3579  r19.2m  3580  r19.2mOLD  3581  r19.3rm  3582  r19.9rmv  3585  rexm  3593  ralm  3597  raaanlem  3598  ifnefalse  3617  ifnotdc  3645  ifandc  3647  ifmdc  3649  nelpri  3694  nelprd  3696  prprc1  3781  difprsn2  3814  diftpsn3  3815  snsssn  3845  preqr2  3853  preq12b  3854  opthpr  3856  prneimg  3858  oprcl  3887  pwprss  3890  intmin4  3957  uniintabim  3966  dfiin2g  4004  iinss2  4024  iundif2ss  4037  disjnim  4079  disjnims  4080  invdisj  4082  disjiun  4084  brne0  4139  brm  4140  trel  4195  trss  4197  ssex  4227  bnd2  4265  abssexg  4274  exmidexmid  4288  rext  4309  unipw  4311  euabex  4319  mss  4320  exss  4321  copsexg  4338  opelopabsb  4356  pwssunim  4383  epelg  4389  sowlin  4419  sotritric  4423  elsuci  4502  sucprc  4511  reusv3  4559  ordon  4586  onsucmin  4607  onsucelsucr  4608  unon  4611  onsucelsucexmid  4630  setind  4639  setind2  4640  sucprcreg  4649  en2lp  4654  eunex  4661  ordsoexmid  4662  ordpwsucss  4667  tfi  4682  peano1  4694  peano2  4695  find  4699  0nelelxp  4756  opelxp  4757  elvvuni  4792  optocl  4804  ralxpf  4878  rexxpf  4879  relop  4882  breldm  4937  reldmm  4952  dmxpm  4954  elreldm  4960  dmrnssfld  4997  dmcosseq  5006  resabs1  5044  resima2  5049  issref  5121  asymref  5124  xpidtr  5129  trin2  5130  poirr2  5131  xpmlem  5159  dmxpss  5169  xp11m  5177  cnveqb  5194  dfco2a  5239  cores2  5251  coi2  5255  relcnvtr  5258  relresfld  5268  relcnvexb  5278  cnviinm  5280  iotauni  5301  iota1  5303  iota4  5308  iotam  5320  dffun8  5356  fununfun  5375  funcnvsn  5377  imadif  5412  imainlem  5413  fcoi1  5519  fcoi2  5520  f0rn0  5534  f1ocnv  5599  f1ocnvb  5600  fun11iun  5607  ffoss  5619  f1o00  5623  fo00  5624  relelfvdm  5674  nfvres  5678  nfunsn  5679  ssimaex  5710  fvmptss2  5724  fvmptssdm  5734  unpreima  5775  respreima  5778  elrnrexdm  5789  elrnrexdmb  5790  rexrnmpt  5793  dffo4  5798  rnmptss  5811  funiun  5832  funopdmsn  5837  fvpr1  5861  fvpr2  5862  elunirn  5912  f1veqaeq  5915  isores1  5960  iotaexel  5981  riotauni  5983  riotacl2  5991  riota1  5996  riota1a  5997  snriota  6008  eusvobj2  6009  acexmidlema  6014  acexmidlemb  6015  acexmidlem2  6020  oprabid  6055  0neqopab  6071  brabvv  6072  1stval2  6323  2ndval2  6324  xp1st  6333  xp2nd  6334  unielxp  6342  releldm2  6353  cnvf1o  6395  fo2ndf  6397  poxp  6402  reldmtpos  6424  dftpos4  6434  tpostpos  6435  tpostpos2  6436  iunon  6455  smoel  6471  tfrlem4  6484  tfrlem7  6488  tfrlem8  6489  tfrlem9  6490  nnaord  6682  ecexr  6712  swoord1  6736  swoord2  6737  0er  6741  mapprc  6826  mapsnconst  6868  ixpf  6894  mptelixpg  6908  idssen  6955  ener  6958  en0  6974  en1  6978  en1bg  6979  2dom  6985  modom  6999  enm  7009  xpsnen  7010  ssenen  7042  snnen2og  7050  php5dom  7054  phpm  7057  findcard  7082  findcard2  7083  findcard2s  7084  unfiexmid  7115  fiintim  7128  fidcenumlemim  7156  sbthlem1  7161  fiss  7181  djuexb  7248  djuss  7274  eldju2ndl  7276  eldju2ndr  7277  ctssdclemr  7316  exmidlpo  7347  finnum  7392  ficardon  7398  exmidfodomrlemim  7417  acnrcl  7421  3nsssucpw1  7459  indpi  7567  subhalfnqq  7639  archnqq  7642  enq0sym  7657  nqnq0pi  7663  nqnq0  7666  mulnnnq0  7675  prml  7702  prmu  7703  prssnql  7704  prssnqu  7705  prcdnql  7709  prcunqu  7710  prltlu  7712  prnmaxl  7713  prnminu  7714  prloc  7716  prdisj  7717  addcanprg  7841  recexprlemopl  7850  recexprlemopu  7852  cauappcvgprlemladdfu  7879  caucvgprlemladdfu  7902  recexgt0sr  7998  renfdisj  8244  axsuploc  8257  negf1o  8566  recexre  8763  apsqgt0  8786  apreim  8788  aprcl  8831  recexaplem2  8837  rerecclap  8915  nn0ge0  9432  elnnnn0b  9451  xnn0xr  9475  xnn0nemnf  9481  xnn0nnn0pnf  9483  znegcl  9515  zeo  9590  nn0ind  9599  nn0ind-raph  9602  uzn0  9777  eluzaddi  9788  eluzsubi  9789  uznn0sub  9793  uz3m2nn  9812  uznnssnn  9816  uz2m1nn  9844  uz2mulcl  9847  indstr2  9848  qmulz  9862  qre  9864  qnegcl  9875  qreccl  9881  rphalflt  9923  nn0ledivnn  10007  xrltnr  10019  nltpnft  10054  ngtmnft  10057  xrrebnd  10059  xnegcl  10072  xnegneg  10073  xltnegi  10075  xrpnfdc  10082  xrmnfdc  10083  xnegid  10099  xaddid1  10102  xnn0lenn0nn0  10105  xnn0xadd0  10107  xposdif  10122  elioore  10152  elfzuz2  10269  uzsubsubfz  10287  fzdisj  10292  fzmmmeqm  10298  elfz0ubfz0  10365  elfz0fzfz0  10366  fz0fzelfz0  10367  fz0fzdiffz0  10370  elfzmlbp  10372  difelfzle  10374  difelfznle  10375  nn0disj  10378  2ffzeq  10381  fzo1fzo0n0  10428  elfzo0z  10429  elfzo0le  10430  fzonmapblen  10432  fzofzim  10433  elfzodifsumelfzo  10452  elfzonlteqm1  10461  fzonn0p1p1  10464  elfzom1p1elfzo  10465  ssfzo12bi  10476  ubmelm1fzo  10477  fzind2  10491  subfzo0  10494  infssuzcldc  10501  rebtwn2z  10520  fldiv4p1lem1div2  10571  fldiv4lem1div2  10573  flqeqceilz  10586  zmodidfzoimp  10622  modfzo0difsn  10663  nnsinds  10713  nn0sinds  10714  expcl2lemap  10819  qexpclz  10828  zzlesq  10976  facp1  10998  facnn2  11002  faclbnd3  11011  bcn1  11026  hashfz0  11095  wrdf  11128  swrdswrdlem  11294  swrdswrd  11295  swrdccatin1  11315  pfxccatin12lem2a  11317  pfxccatin12lem1  11318  swrdccatin2  11319  pfxccatin12lem2  11321  pfxccatin12lem3  11322  pfxccatin12  11323  pfxccat3  11324  swrdccat  11325  swrdccat3blem  11329  cvg1nlemres  11568  rexanuz  11571  fclim  11877  climmo  11881  iser3shft  11929  fsumsplitsn  11994  fsum2dlemstep  12018  fisumcom2  12022  arisum  12082  arisum2  12083  prodmodc  12162  fprodfac  12199  fprod2dlemstep  12206  fprodcom2fi  12210  fprodsplitsn  12217  eftlub  12274  ef01bndlem  12340  sin01gt0  12346  cos01gt0  12347  sin02gt0  12348  dvdsdivcl  12434  addmodlteqALT  12443  odd2np1  12457  oddge22np1  12465  m1expe  12483  nn0enne  12486  nn0o1gt2  12489  nno  12490  ndvdsadd  12515  dfgcd2  12608  mulgcd  12610  algfx  12647  prmind2  12715  prm2orodd  12721  prmgt1  12727  oddprmgt2  12729  dfphi2  12815  nnnn0modprm0  12851  prm23lt5  12859  pythagtriplem2  12862  pcz  12928  dvdsprmpweqnn  12932  oddprmdvds  12950  prmunb  12958  4sqlem4  12988  4sqlem19  13005  evenennn  13037  fngsum  13494  igsumvalx  13495  dfgrp3me  13706  mulgnn0gsum  13738  rngdi  13977  rngdir  13978  dvdsrcl2  14137  unitinvcl  14161  unitinvinv  14162  unitlinv  14164  unitrinv  14165  rmodislmodlem  14388  rmodislmod  14389  zrhval  14655  psrbagf  14708  distop  14838  ntrss  14872  ssntr  14875  lmrcl  14945  txuni2  15009  txcn  15028  hmeocnvb  15071  xmetunirn  15111  blssioo  15306  divcnap  15318  cdivcncfap  15357  dedekindeulemlub  15373  dedekindicclemlub  15382  dvexp2  15465  elply2  15488  plyco  15512  pilem3  15536  sincosq1sgn  15579  sincosq2sgn  15580  sincosq3sgn  15581  sincosq4sgn  15582  sinq12gt0  15583  fsumdvdsmul  15744  zabsle1  15757  lgsdir2lem4  15789  gausslemma2dlem0f  15812  gausslemma2dlem1a  15816  gausslemma2dlem2  15820  gausslemma2dlem3  15821  gausslemma2dlem4  15822  2lgslem1a1  15844  2lgslem3  15859  2lgsoddprmlem3  15869  2lgsoddprm  15871  2sqlem2  15873  2sqlem10  15883  vtxvalprc  15935  iedgvalprc  15936  upgrex  15983  umgredg  16025  ausgrusgrben  16048  usgruspgrben  16066  usgrislfuspgrdom  16070  uhgr2edg  16086  uspgredg2v  16101  griedg0ssusgr  16131  subusgr  16155  wlkv  16206  wlk1walkdom  16239  trlsv  16264  trlf1  16268  clwwlk1loop  16279  clwwlkext2edg  16302  umgr2cwwkdifex  16305  clwwlknonex2lem2  16318  clwwlknonex2e  16320  eupthv  16326  eupth2lem3lem4fi  16353  konigsberglem5  16372  bj-pm2.18st  16407  bj-dcstab  16413  decidi  16452  sumdc2  16456  bj-charfunbi  16466  bdel  16500  bdssex  16557  bj-indind  16587  findset  16600  nninfall  16674  trirec0  16715  neap0mkv  16741