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  565  an32s  568  an4s  590  sylnbi  682  dcim  845  notnotrdc  847  condcOLD  858  pm2.61ddc  865  pm5.18dc  887  pm2.25dc  897  pm2.85dc  909  pm5.12dc  914  pm5.14dc  915  pm5.55dc  917  peircedc  918  pm5.54dc  922  dcand  937  dcor  940  pm5.62dc  950  pm5.63dc  951  pm4.83dc  956  3simpb  1000  3simpc  1001  3imp  1198  3com12  1212  3com13  1213  syl3anb  1295  xoranor  1399  xorbin  1406  xordc1  1415  biassdc  1417  nfr  1544  nfand  1594  19.21t  1608  19.30dc  1653  exintrbi  1659  19.9t  1668  nfnt  1682  equveli  1785  exdistrfor  1826  sbcof2  1836  sbidm  1877  sbi1v  1918  sbalyz  2030  sbal1yz  2032  nfsb4t  2045  euex  2087  eumo0  2088  mor  2100  exmodc  2108  mo3h  2111  mopick  2136  moexexdc  2142  euexex  2143  2euex  2145  exists2  2155  eqcoms  2212  eleq2s  2304  nfcr  2344  necon3ai  2429  rexnalim  2499  dfrex2dc  2501  rexex  2556  rsp  2557  ralim  2569  rexim  2604  r19.32r  2657  r19.44av  2670  r19.45av  2671  gencl  2812  gencbvex  2827  gencbval  2829  vtoclgf  2839  vtoclg1f  2840  pm13.183  2921  elrabi  2936  eueq2dc  2956  eueq3dc  2957  mob2  2963  euxfr2dc  2968  reu3  2973  rmoim  2984  2rmorex  2989  sbcex  3017  sbcbi2  3059  ra5  3098  sseq1  3227  difdif  3309  dfss4st  3417  difindiss  3438  undif3ss  3445  dfrab3ss  3462  abvor0dc  3495  reldisj  3523  disjel  3526  inssdif0im  3539  uneqdifeqim  3557  r19.2m  3558  r19.2mOLD  3559  r19.3rm  3560  r19.9rmv  3563  rexm  3571  ralm  3575  raaanlem  3576  ifnefalse  3593  ifnotdc  3621  ifandc  3623  ifmdc  3625  nelpri  3670  nelprd  3672  prprc1  3754  difprsn2  3787  diftpsn3  3788  snsssn  3818  preqr2  3826  preq12b  3827  opthpr  3829  prneimg  3831  oprcl  3860  pwprss  3863  intmin4  3930  uniintabim  3939  dfiin2g  3977  iinss2  3997  iundif2ss  4010  disjnim  4052  disjnims  4053  invdisj  4055  disjiun  4057  brne0  4112  brm  4113  trel  4168  trss  4170  ssex  4200  bnd2  4236  abssexg  4245  exmidexmid  4259  rext  4280  unipw  4282  euabex  4290  mss  4291  exss  4292  copsexg  4309  opelopabsb  4327  pwssunim  4352  epelg  4358  sowlin  4388  sotritric  4392  elsuci  4471  sucprc  4480  reusv3  4528  ordon  4555  onsucmin  4576  onsucelsucr  4577  unon  4580  onsucelsucexmid  4599  setind  4608  setind2  4609  sucprcreg  4618  en2lp  4623  eunex  4630  ordsoexmid  4631  ordpwsucss  4636  tfi  4651  peano1  4663  peano2  4664  find  4668  0nelelxp  4725  opelxp  4726  elvvuni  4760  optocl  4772  ralxpf  4845  rexxpf  4846  relop  4849  breldm  4904  dmxpm  4920  elreldm  4926  dmrnssfld  4963  dmcosseq  4972  resabs1  5010  resima2  5015  issref  5087  asymref  5090  xpidtr  5095  trin2  5096  poirr2  5097  xpmlem  5125  dmxpss  5135  xp11m  5143  cnveqb  5160  dfco2a  5205  cores2  5217  coi2  5221  relcnvtr  5224  relresfld  5234  relcnvexb  5244  cnviinm  5246  iotauni  5267  iota1  5269  iota4  5274  iotam  5286  dffun8  5322  fununfun  5340  funcnvsn  5342  imadif  5377  imainlem  5378  fcoi1  5482  fcoi2  5483  f0rn0  5496  f1ocnv  5561  f1ocnvb  5562  fun11iun  5569  ffoss  5580  f1o00  5584  fo00  5585  relelfvdm  5635  nfvres  5637  nfunsn  5638  ssimaex  5668  fvmptss2  5682  fvmptssdm  5692  unpreima  5733  respreima  5736  elrnrexdm  5747  elrnrexdmb  5748  rexrnmpt  5751  dffo4  5756  rnmptss  5769  funiun  5789  funopdmsn  5792  fvpr1  5816  fvpr2  5817  elunirn  5863  f1veqaeq  5866  isores1  5911  iotaexel  5932  riotauni  5934  riotacl2  5942  riota1  5947  riota1a  5948  snriota  5959  eusvobj2  5960  acexmidlema  5965  acexmidlemb  5966  acexmidlem2  5971  oprabid  6006  0neqopab  6020  brabvv  6021  1stval2  6271  2ndval2  6272  xp1st  6281  xp2nd  6282  unielxp  6290  releldm2  6301  cnvf1o  6341  fo2ndf  6343  poxp  6348  reldmtpos  6369  dftpos4  6379  tpostpos  6380  tpostpos2  6381  iunon  6400  smoel  6416  tfrlem4  6429  tfrlem7  6433  tfrlem8  6434  tfrlem9  6435  nnaord  6625  ecexr  6655  swoord1  6679  swoord2  6680  0er  6684  mapprc  6769  mapsnconst  6811  ixpf  6837  mptelixpg  6851  idssen  6898  ener  6901  en0  6917  en1  6921  en1bg  6922  2dom  6928  enm  6947  xpsnen  6948  ssenen  6980  snnen2og  6988  php5dom  6992  phpm  6995  findcard  7018  findcard2  7019  findcard2s  7020  unfiexmid  7048  fiintim  7061  fidcenumlemim  7087  sbthlem1  7092  fiss  7112  djuexb  7179  djuss  7205  eldju2ndl  7207  eldju2ndr  7208  ctssdclemr  7247  exmidlpo  7278  finnum  7323  ficardon  7329  exmidfodomrlemim  7347  acnrcl  7351  3nsssucpw1  7389  indpi  7497  subhalfnqq  7569  archnqq  7572  enq0sym  7587  nqnq0pi  7593  nqnq0  7596  mulnnnq0  7605  prml  7632  prmu  7633  prssnql  7634  prssnqu  7635  prcdnql  7639  prcunqu  7640  prltlu  7642  prnmaxl  7643  prnminu  7644  prloc  7646  prdisj  7647  addcanprg  7771  recexprlemopl  7780  recexprlemopu  7782  cauappcvgprlemladdfu  7809  caucvgprlemladdfu  7832  recexgt0sr  7928  renfdisj  8174  axsuploc  8187  negf1o  8496  recexre  8693  apsqgt0  8716  apreim  8718  aprcl  8761  recexaplem2  8767  rerecclap  8845  nn0ge0  9362  elnnnn0b  9381  xnn0xr  9405  xnn0nemnf  9411  xnn0nnn0pnf  9413  znegcl  9445  zeo  9520  nn0ind  9529  nn0ind-raph  9532  uzn0  9706  eluzaddi  9717  eluzsubi  9718  uznn0sub  9722  uz3m2nn  9736  uznnssnn  9740  uz2m1nn  9768  uz2mulcl  9771  indstr2  9772  qmulz  9786  qre  9788  qnegcl  9799  qreccl  9805  rphalflt  9847  nn0ledivnn  9931  xrltnr  9943  nltpnft  9978  ngtmnft  9981  xrrebnd  9983  xnegcl  9996  xnegneg  9997  xltnegi  9999  xrpnfdc  10006  xrmnfdc  10007  xnegid  10023  xaddid1  10026  xnn0lenn0nn0  10029  xnn0xadd0  10031  xposdif  10046  elioore  10076  elfzuz2  10193  uzsubsubfz  10211  fzdisj  10216  fzmmmeqm  10222  elfz0ubfz0  10289  elfz0fzfz0  10290  fz0fzelfz0  10291  fz0fzdiffz0  10294  elfzmlbp  10296  difelfzle  10298  difelfznle  10299  nn0disj  10302  2ffzeq  10305  fzo1fzo0n0  10351  elfzo0z  10352  elfzo0le  10353  fzonmapblen  10355  fzofzim  10356  elfzodifsumelfzo  10374  elfzonlteqm1  10383  fzonn0p1p1  10386  elfzom1p1elfzo  10387  ssfzo12bi  10398  ubmelm1fzo  10399  fzind2  10412  subfzo0  10415  infssuzcldc  10422  rebtwn2z  10441  fldiv4p1lem1div2  10492  fldiv4lem1div2  10494  flqeqceilz  10507  zmodidfzoimp  10543  modfzo0difsn  10584  nnsinds  10634  nn0sinds  10635  expcl2lemap  10740  qexpclz  10749  zzlesq  10897  facp1  10919  facnn2  10923  faclbnd3  10932  bcn1  10947  hashfz0  11014  wrdf  11044  swrdswrdlem  11202  swrdswrd  11203  swrdccatin1  11223  pfxccatin12lem2a  11225  pfxccatin12lem1  11226  swrdccatin2  11227  pfxccatin12lem2  11229  pfxccatin12lem3  11230  pfxccatin12  11231  pfxccat3  11232  swrdccat  11233  swrdccat3blem  11237  cvg1nlemres  11462  rexanuz  11465  fclim  11771  climmo  11775  iser3shft  11823  fsumsplitsn  11887  fsum2dlemstep  11911  fisumcom2  11915  arisum  11975  arisum2  11976  prodmodc  12055  fprodfac  12092  fprod2dlemstep  12099  fprodcom2fi  12103  fprodsplitsn  12110  eftlub  12167  ef01bndlem  12233  sin01gt0  12239  cos01gt0  12240  sin02gt0  12241  dvdsdivcl  12327  addmodlteqALT  12336  odd2np1  12350  oddge22np1  12358  m1expe  12376  nn0enne  12379  nn0o1gt2  12382  nno  12383  ndvdsadd  12408  dfgcd2  12501  mulgcd  12503  algfx  12540  prmind2  12608  prm2orodd  12614  prmgt1  12620  oddprmgt2  12622  dfphi2  12708  nnnn0modprm0  12744  prm23lt5  12752  pythagtriplem2  12755  pcz  12821  dvdsprmpweqnn  12825  oddprmdvds  12843  prmunb  12851  4sqlem4  12881  4sqlem19  12898  evenennn  12930  fngsum  13387  igsumvalx  13388  dfgrp3me  13599  mulgnn0gsum  13631  rngdi  13869  rngdir  13870  dvdsrcl2  14028  unitinvcl  14052  unitinvinv  14053  unitlinv  14055  unitrinv  14056  rmodislmodlem  14279  rmodislmod  14280  zrhval  14546  psrbagf  14599  distop  14724  ntrss  14758  ssntr  14761  lmrcl  14830  lmreltop  14832  txuni2  14895  txcn  14914  hmeocnvb  14957  xmetunirn  14997  blssioo  15192  divcnap  15204  cdivcncfap  15243  dedekindeulemlub  15259  dedekindicclemlub  15268  dvexp2  15351  elply2  15374  plyco  15398  pilem3  15422  sincosq1sgn  15465  sincosq2sgn  15466  sincosq3sgn  15467  sincosq4sgn  15468  sinq12gt0  15469  fsumdvdsmul  15630  zabsle1  15643  lgsdir2lem4  15675  gausslemma2dlem0f  15698  gausslemma2dlem1a  15702  gausslemma2dlem2  15706  gausslemma2dlem3  15707  gausslemma2dlem4  15708  2lgslem1a1  15730  2lgslem3  15745  2lgsoddprmlem3  15755  2lgsoddprm  15757  2sqlem2  15759  2sqlem10  15769  vtxvalprc  15821  iedgvalprc  15822  upgrex  15868  umgredg  15908  ausgrusgrben  15931  usgruspgrben  15949  usgrislfuspgrdom  15953  uhgr2edg  15969  uspgredg2v  15984  bj-pm2.18st  16024  bj-dcstab  16030  decidi  16069  sumdc2  16073  bj-charfunbi  16084  bdel  16118  bdssex  16175  bj-indind  16205  findset  16218  nninfall  16286  trirec0  16323  neap0mkv  16348