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  391  mpan10  478  an12s  571  an32s  574  an4s  596  sylnbi  689  dcim  853  notnotrdc  855  condcOLD  866  pm2.61ddc  873  pm5.18dc  895  pm2.25dc  905  pm2.85dc  917  pm5.12dc  922  pm5.14dc  923  pm5.55dc  925  peircedc  926  pm5.54dc  930  dcand  945  dcor  948  pm5.62dc  958  pm5.63dc  959  pm4.83dc  964  ifp2  993  ifpor  1000  1fpid3  1007  3simpb  1026  3simpc  1027  3imp  1224  3com12  1238  3com13  1239  syl3anb  1321  xoranor  1426  xorbin  1433  xordc1  1442  biassdc  1444  nfr  1571  nfand  1621  19.21t  1635  19.30dc  1680  exintrbi  1686  19.9t  1695  nfnt  1708  equveli  1812  exdistrfor  1853  sbcof2  1863  sbidm  1904  sbi1v  1946  sbalyz  2059  sbal1yz  2061  nfsb4t  2074  euex  2116  eumo0  2117  mor  2129  exmodc  2137  mo3h  2140  mopick  2165  moexexdc  2171  euexex  2172  2euex  2174  exists2  2184  eqcoms  2241  eleq2s  2333  nfcr  2384  necon3ai  2469  rexnalim  2539  dfrex2dc  2541  rexex  2596  rsp  2597  ralim  2609  rexim  2644  r19.32r  2697  r19.44av  2710  r19.45av  2711  gencl  2854  gencbvex  2869  gencbval  2871  vtoclgf  2881  vtoclg1f  2882  pm13.183  2964  elrabi  2979  eueq2dc  2999  eueq3dc  3000  mob2  3006  euxfr2dc  3011  reu3  3016  rmoim  3027  2rmorex  3032  sbcex  3060  sbcbi2  3102  ra5  3141  sseq1  3271  difdif  3354  dfss4st  3464  difindiss  3485  undif3ss  3492  dfrab3ss  3511  abvor0dc  3545  reldisj  3576  disjel  3579  inssdif0imOLD  3593  uneqdifeqim  3613  r19.2m  3614  r19.2mOLD  3615  r19.3rm  3616  r19.9rmv  3619  rexm  3627  ralm  3631  raaanlem  3632  ifnefalse  3651  ifnotdc  3679  ifandc  3681  ifmdc  3683  nelpri  3732  nelprd  3734  prprc1  3819  difprsn2  3853  diftpsn3  3854  snsssn  3884  preqr2  3892  preq12b  3893  opthpr  3895  prneimg  3897  oprcl  3926  pwprss  3929  intmin4  3996  uniintabim  4005  dfiin2g  4043  iinss2  4063  iundif2ss  4076  disjnim  4118  disjnims  4119  invdisj  4121  disjiun  4123  brne0  4178  brm  4179  trel  4234  trss  4236  ssex  4268  bnd2  4308  abssexg  4317  exmidexmid  4331  rext  4353  unipw  4355  euabex  4363  mss  4364  exss  4365  copsexg  4382  opelopabsb  4400  pwssunim  4427  epelg  4433  sowlin  4463  sotritric  4467  elsuci  4546  sucprc  4555  reusv3  4604  ordon  4631  onsucmin  4652  onsucelsucr  4653  unon  4656  onsucelsucexmid  4675  setind  4684  setind2  4685  sucprcreg  4694  en2lp  4699  eunex  4706  ordsoexmid  4707  ordpwsucss  4712  tfi  4727  peano1  4739  peano2  4740  find  4744  0nelelxp  4801  opelxp  4802  elvvuni  4837  optocl  4849  ralxpf  4924  rexxpf  4925  relop  4928  breldm  4983  reldmm  4998  dmxpm  5000  elreldm  5006  dmrnssfld  5043  dmcosseq  5052  resabs1  5090  resima2  5095  issref  5168  asymref  5171  xpidtr  5176  trin2  5177  poirr2  5178  xpmlem  5206  dmxpss  5216  xp11m  5224  cnveqb  5241  dfco2a  5286  cores2  5298  coi2  5302  relcnvtr  5305  relresfld  5315  relcnvexb  5325  cnviinm  5327  iotauni  5348  iota1  5350  iota4  5355  iotam  5367  dffun8  5403  fununfun  5422  funcnvsn  5424  imadif  5459  imainlem  5460  fcoi1  5570  fcoi2  5571  f0rn0  5585  f1ocnv  5650  f1ocnvb  5651  fun11iun  5658  ffoss  5670  f1o00  5674  fo00  5675  relelfvdm  5725  nfvres  5729  nfunsn  5730  ssimaex  5761  fvmptss2  5777  fvmptssdm  5787  unpreima  5827  respreima  5830  elrnrexdm  5841  elrnrexdmb  5842  rexrnmpt  5845  dffo4  5850  rnmptss  5863  funiun  5884  funopdmsn  5889  fvpr1  5913  fvpr2  5914  elunirn  5966  f1veqaeq  5969  isores1  6014  iotaexel  6037  riotauni  6039  riotacl2  6047  riota1  6052  riota1a  6053  snriota  6064  eusvobj2  6065  acexmidlema  6070  acexmidlemb  6071  acexmidlem2  6076  oprabid  6111  0neqopab  6127  brabvv  6128  1stval2  6383  2ndval2  6384  xp1st  6393  xp2nd  6394  unielxp  6402  releldm2  6413  cnvf1o  6455  fo2ndf  6457  poxp  6462  reldmtpos  6518  dftpos4  6528  tpostpos  6529  tpostpos2  6530  iunon  6549  smoel  6565  tfrlem4  6578  tfrlem7  6582  tfrlem8  6583  tfrlem9  6584  nnaord  6776  ecexr  6806  swoord1  6830  swoord2  6831  0er  6835  mapprc  6920  mapfoss  6941  fsetdmprc0  6944  mapsnconst  6970  ixpf  6996  mptelixpg  7010  idssen  7057  ener  7060  en0  7076  en1  7080  en1bg  7081  2dom  7087  modom  7102  enm  7112  xpsnen  7113  ssenen  7146  snnen2og  7154  php5dom  7158  phpm  7161  findcard  7186  findcard2  7187  findcard2s  7188  unfiexmid  7219  fiintim  7232  fidcenumlemim  7263  sbthlem1  7268  fiss  7305  djuexb  7378  djuss  7404  eldju2ndl  7406  eldju2ndr  7407  ctssdclemr  7446  exmidlpo  7477  finnum  7522  ficardon  7528  exmidfodomrlemim  7547  acnrcl  7551  3nsssucpw1  7589  indpi  7703  subhalfnqq  7775  archnqq  7778  enq0sym  7793  nqnq0pi  7799  nqnq0  7802  mulnnnq0  7811  prml  7838  prmu  7839  prssnql  7840  prssnqu  7841  prcdnql  7845  prcunqu  7846  prltlu  7848  prnmaxl  7849  prnminu  7850  prloc  7852  prdisj  7853  addcanprg  7977  recexprlemopl  7986  recexprlemopu  7988  cauappcvgprlemladdfu  8015  caucvgprlemladdfu  8038  recexgt0sr  8134  renfdisj  8379  axsuploc  8392  negf1o  8703  recexre  8900  apsqgt0  8923  apreim  8925  aprcl  8968  recexaplem2  8974  rerecclap  9054  nn0ge0  9571  elnnnn0b  9590  xnn0xr  9618  xnn0nemnf  9624  xnn0nnn0pnf  9626  znegcl  9658  zeo  9734  nn0ind  9743  nn0ind-raph  9746  uzn0  9921  eluzaddi  9932  eluzsubi  9933  uznn0sub  9937  uz3m2nn  9956  uznnssnn  9960  uz2m1nn  9988  uz2mulcl  9991  indstr2  9992  qmulz  10006  qre  10008  qnegcl  10019  qreccl  10025  rphalflt  10067  nn0ledivnn  10151  xrltnr  10164  nltpnft  10199  ngtmnft  10202  xrrebnd  10204  xnegcl  10217  xnegneg  10218  xltnegi  10220  xrpnfdc  10227  xrmnfdc  10228  xnegid  10244  xaddid1  10247  xnn0lenn0nn0  10250  xnn0xadd0  10252  xposdif  10267  elioore  10297  elfzuz2  10416  uzsubsubfz  10435  fzdisj  10440  fzmmmeqm  10447  elfz0ubfz0  10515  elfz0fzfz0  10516  fz0fzelfz0  10517  fz0fzdiffz0  10520  elfzmlbp  10522  difelfzle  10524  difelfznle  10525  nn0disj  10528  2ffzeq  10531  fzo1fzo0n0  10578  elfzo0z  10579  elfzo0le  10580  fzonmapblen  10582  fzofzim  10583  elfzodifsumelfzo  10602  elfzonlteqm1  10611  fzonn0p1p1  10614  elfzom1p1elfzo  10615  ssfzo12bi  10626  ubmelm1fzo  10627  fzind2  10641  subfzo0  10644  infssuzcldc  10651  rebtwn2z  10672  fldiv4p1lem1div2  10723  fldiv4lem1div2  10725  flqeqceilz  10738  zmodidfzoimp  10774  modfzo0difsn  10815  nnsinds  10865  nn0sinds  10866  expcl2lemap  10971  qexpclz  10980  zzlesq  11129  facp1  11151  facnn2  11155  faclbnd3  11164  bcn1  11179  hashfz0  11249  hashfibc  11266  hashf1lem2  11269  wrdf  11293  swrdswrdlem  11459  swrdswrd  11460  swrdccatin1  11480  pfxccatin12lem2a  11482  pfxccatin12lem1  11483  swrdccatin2  11484  pfxccatin12lem2  11486  pfxccatin12lem3  11487  pfxccatin12  11488  pfxccat3  11489  swrdccat  11490  swrdccat3blem  11494  cvg1nlemres  11734  rexanuz  11737  fclim  12043  climmo  12047  iser3shft  12095  fsumsplitsn  12160  fsum2dlemstep  12184  fisumcom2  12188  arisum  12248  arisum2  12249  prodmodc  12328  fprodfac  12365  fprod2dlemstep  12372  fprodcom2fi  12376  fprodsplitsn  12383  eftlub  12440  ef01bndlem  12506  sin01gt0  12512  cos01gt0  12513  sin02gt0  12514  dvdsdivcl  12600  addmodlteqALT  12609  odd2np1  12623  oddge22np1  12631  m1expe  12649  nn0enne  12652  nn0o1gt2  12655  nno  12656  ndvdsadd  12681  dfgcd2  12774  mulgcd  12776  algfx  12813  prmind2  12881  prm2orodd  12887  prmgt1  12893  oddprmgt2  12895  dfphi2  12981  nnnn0modprm0  13017  prm23lt5  13025  pythagtriplem2  13028  pcz  13094  dvdsprmpweqnn  13098  oddprmdvds  13116  prmunb  13124  4sqlem4  13154  4sqlem19  13171  ballotfilem2  13211  ballotfilem7  13262  evenennn  13267  fngzsum  13691  gzsumvalx  13692  dfgrp3me  13888  mulgnn0gzsum  13914  rngdi  14222  rngdir  14223  dvdsrcl2  14389  unitinvcl  14413  unitinvinv  14414  unitlinv  14416  unitrinv  14417  opprdrng  14603  rmodislmodlem  14670  rmodislmod  14671  zrhval  14935  psrbagf  15037  distop  15169  ntrss  15203  ssntr  15206  lmrcl  15276  txuni2  15340  txcn  15359  hmeocnvb  15402  xmetunirn  15442  blssioo  15637  divcnap  15649  cdivcncfap  15688  dedekindeulemlub  15704  dedekindicclemlub  15713  dvexp2  15796  elply2  15819  plyco  15843  pilem3  15867  sincosq1sgn  15910  sincosq2sgn  15911  sincosq3sgn  15912  sincosq4sgn  15913  sinq12gt0  15914  logfac  15978  birthdaylem1g  16070  fsumdvdsmul  16088  zabsle1  16101  lgsdir2lem4  16133  gausslemma2dlem0f  16156  gausslemma2dlem1a  16160  gausslemma2dlem2  16164  gausslemma2dlem3  16165  gausslemma2dlem4  16166  2lgslem1a1  16188  2lgslem3  16203  2lgsoddprmlem3  16213  2lgsoddprm  16215  2sqlem2  16217  2sqlem10  16227  vtxvalprc  16279  iedgvalprc  16280  upgrex  16327  umgredg  16369  ausgrusgrben  16392  usgruspgrben  16410  usgrislfuspgrdom  16414  uhgr2edg  16430  uspgredg2v  16445  griedg0ssusgr  16475  subusgr  16499  wlkv  16550  wlk1walkdom  16583  trlsv  16608  trlf1  16612  clwwlk1loop  16623  clwwlkext2edg  16646  umgr2cwwkdifex  16649  clwwlknonex2lem2  16662  clwwlknonex2e  16664  eupthv  16670  eupth2lem3lem4fi  16697  konigsberglem5  16716  bj-pm2.18st  16761  bj-dcstab  16767  decidi  16806  sumdc2  16810  bj-charfunbi  16820  bdel  16854  bdssex  16911  bj-indind  16941  findset  16954  nninfall  17026  trirec0  17067  neap0mkv  17093  alsex  17113  ralsex  17114