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  685  dcim  849  notnotrdc  851  condcOLD  862  pm2.61ddc  869  pm5.18dc  891  pm2.25dc  901  pm2.85dc  913  pm5.12dc  918  pm5.14dc  919  pm5.55dc  921  peircedc  922  pm5.54dc  926  dcand  941  dcor  944  pm5.62dc  954  pm5.63dc  955  pm4.83dc  960  ifp2  989  ifpor  996  1fpid3  1003  3simpb  1022  3simpc  1023  3imp  1220  3com12  1234  3com13  1235  syl3anb  1317  xoranor  1422  xorbin  1429  xordc1  1438  biassdc  1440  nfr  1567  nfand  1617  19.21t  1631  19.30dc  1676  exintrbi  1682  19.9t  1691  nfnt  1704  equveli  1808  exdistrfor  1849  sbcof2  1859  sbidm  1900  sbi1v  1941  sbalyz  2053  sbal1yz  2055  nfsb4t  2068  euex  2110  eumo0  2111  mor  2123  exmodc  2131  mo3h  2134  mopick  2159  moexexdc  2165  euexex  2166  2euex  2168  exists2  2178  eqcoms  2235  eleq2s  2327  nfcr  2376  necon3ai  2461  rexnalim  2531  dfrex2dc  2533  rexex  2588  rsp  2589  ralim  2601  rexim  2636  r19.32r  2689  r19.44av  2702  r19.45av  2703  gencl  2845  gencbvex  2860  gencbval  2862  vtoclgf  2872  vtoclg1f  2873  pm13.183  2954  elrabi  2969  eueq2dc  2989  eueq3dc  2990  mob2  2996  euxfr2dc  3001  reu3  3006  rmoim  3017  2rmorex  3022  sbcex  3050  sbcbi2  3092  ra5  3131  sseq1  3260  difdif  3343  dfss4st  3453  difindiss  3474  undif3ss  3481  dfrab3ss  3498  abvor0dc  3531  reldisj  3559  disjel  3562  inssdif0im  3575  uneqdifeqim  3594  r19.2m  3595  r19.2mOLD  3596  r19.3rm  3597  r19.9rmv  3600  rexm  3608  ralm  3612  raaanlem  3613  ifnefalse  3632  ifnotdc  3660  ifandc  3662  ifmdc  3664  nelpri  3712  nelprd  3714  prprc1  3799  difprsn2  3833  diftpsn3  3834  snsssn  3864  preqr2  3872  preq12b  3873  opthpr  3875  prneimg  3877  oprcl  3906  pwprss  3909  intmin4  3976  uniintabim  3985  dfiin2g  4023  iinss2  4043  iundif2ss  4056  disjnim  4098  disjnims  4099  invdisj  4101  disjiun  4103  brne0  4158  brm  4159  trel  4214  trss  4216  ssex  4246  bnd2  4285  abssexg  4294  exmidexmid  4308  rext  4330  unipw  4332  euabex  4340  mss  4341  exss  4342  copsexg  4359  opelopabsb  4377  pwssunim  4404  epelg  4410  sowlin  4440  sotritric  4444  elsuci  4523  sucprc  4532  reusv3  4580  ordon  4607  onsucmin  4628  onsucelsucr  4629  unon  4632  onsucelsucexmid  4651  setind  4660  setind2  4661  sucprcreg  4670  en2lp  4675  eunex  4682  ordsoexmid  4683  ordpwsucss  4688  tfi  4703  peano1  4715  peano2  4716  find  4720  0nelelxp  4777  opelxp  4778  elvvuni  4813  optocl  4825  ralxpf  4900  rexxpf  4901  relop  4904  breldm  4959  reldmm  4974  dmxpm  4976  elreldm  4982  dmrnssfld  5019  dmcosseq  5028  resabs1  5066  resima2  5071  issref  5144  asymref  5147  xpidtr  5152  trin2  5153  poirr2  5154  xpmlem  5182  dmxpss  5192  xp11m  5200  cnveqb  5217  dfco2a  5262  cores2  5274  coi2  5278  relcnvtr  5281  relresfld  5291  relcnvexb  5301  cnviinm  5303  iotauni  5324  iota1  5326  iota4  5331  iotam  5343  dffun8  5379  fununfun  5398  funcnvsn  5400  imadif  5435  imainlem  5436  fcoi1  5546  fcoi2  5547  f0rn0  5561  f1ocnv  5626  f1ocnvb  5627  fun11iun  5634  ffoss  5646  f1o00  5650  fo00  5651  relelfvdm  5701  nfvres  5705  nfunsn  5706  ssimaex  5737  fvmptss2  5751  fvmptssdm  5761  unpreima  5801  respreima  5804  elrnrexdm  5815  elrnrexdmb  5816  rexrnmpt  5819  dffo4  5824  rnmptss  5837  funiun  5858  funopdmsn  5863  fvpr1  5887  fvpr2  5888  elunirn  5938  f1veqaeq  5941  isores1  5986  iotaexel  6007  riotauni  6009  riotacl2  6017  riota1  6022  riota1a  6023  snriota  6034  eusvobj2  6035  acexmidlema  6040  acexmidlemb  6041  acexmidlem2  6046  oprabid  6081  0neqopab  6097  brabvv  6098  1stval2  6348  2ndval2  6349  xp1st  6358  xp2nd  6359  unielxp  6367  releldm2  6378  cnvf1o  6420  fo2ndf  6422  poxp  6427  reldmtpos  6483  dftpos4  6493  tpostpos  6494  tpostpos2  6495  iunon  6514  smoel  6530  tfrlem4  6543  tfrlem7  6547  tfrlem8  6548  tfrlem9  6549  nnaord  6741  ecexr  6771  swoord1  6795  swoord2  6796  0er  6800  mapprc  6885  mapsnconst  6928  ixpf  6954  mptelixpg  6968  idssen  7015  ener  7018  en0  7034  en1  7038  en1bg  7039  2dom  7045  modom  7060  enm  7070  xpsnen  7071  ssenen  7104  snnen2og  7112  php5dom  7116  phpm  7119  findcard  7144  findcard2  7145  findcard2s  7146  unfiexmid  7177  fiintim  7190  fidcenumlemim  7221  sbthlem1  7226  fiss  7263  djuexb  7334  djuss  7360  eldju2ndl  7362  eldju2ndr  7363  ctssdclemr  7402  exmidlpo  7433  finnum  7478  ficardon  7484  exmidfodomrlemim  7503  acnrcl  7507  3nsssucpw1  7545  indpi  7653  subhalfnqq  7725  archnqq  7728  enq0sym  7743  nqnq0pi  7749  nqnq0  7752  mulnnnq0  7761  prml  7788  prmu  7789  prssnql  7790  prssnqu  7791  prcdnql  7795  prcunqu  7796  prltlu  7798  prnmaxl  7799  prnminu  7800  prloc  7802  prdisj  7803  addcanprg  7927  recexprlemopl  7936  recexprlemopu  7938  cauappcvgprlemladdfu  7965  caucvgprlemladdfu  7988  recexgt0sr  8084  renfdisj  8329  axsuploc  8342  negf1o  8651  recexre  8848  apsqgt0  8871  apreim  8873  aprcl  8916  recexaplem2  8922  rerecclap  9000  nn0ge0  9517  elnnnn0b  9536  xnn0xr  9564  xnn0nemnf  9570  xnn0nnn0pnf  9572  znegcl  9604  zeo  9679  nn0ind  9688  nn0ind-raph  9691  uzn0  9866  eluzaddi  9877  eluzsubi  9878  uznn0sub  9882  uz3m2nn  9901  uznnssnn  9905  uz2m1nn  9933  uz2mulcl  9936  indstr2  9937  qmulz  9951  qre  9953  qnegcl  9964  qreccl  9970  rphalflt  10012  nn0ledivnn  10096  xrltnr  10108  nltpnft  10143  ngtmnft  10146  xrrebnd  10148  xnegcl  10161  xnegneg  10162  xltnegi  10164  xrpnfdc  10171  xrmnfdc  10172  xnegid  10188  xaddid1  10191  xnn0lenn0nn0  10194  xnn0xadd0  10196  xposdif  10211  elioore  10241  elfzuz2  10359  uzsubsubfz  10377  fzdisj  10382  fzmmmeqm  10388  elfz0ubfz0  10455  elfz0fzfz0  10456  fz0fzelfz0  10457  fz0fzdiffz0  10460  elfzmlbp  10462  difelfzle  10464  difelfznle  10465  nn0disj  10468  2ffzeq  10471  fzo1fzo0n0  10518  elfzo0z  10519  elfzo0le  10520  fzonmapblen  10522  fzofzim  10523  elfzodifsumelfzo  10542  elfzonlteqm1  10551  fzonn0p1p1  10554  elfzom1p1elfzo  10555  ssfzo12bi  10566  ubmelm1fzo  10567  fzind2  10581  subfzo0  10584  infssuzcldc  10591  rebtwn2z  10610  fldiv4p1lem1div2  10661  fldiv4lem1div2  10663  flqeqceilz  10676  zmodidfzoimp  10712  modfzo0difsn  10753  nnsinds  10803  nn0sinds  10804  expcl2lemap  10909  qexpclz  10918  zzlesq  11066  facp1  11088  facnn2  11092  faclbnd3  11101  bcn1  11116  hashfz0  11185  hashfibc  11200  wrdf  11223  swrdswrdlem  11389  swrdswrd  11390  swrdccatin1  11410  pfxccatin12lem2a  11412  pfxccatin12lem1  11413  swrdccatin2  11414  pfxccatin12lem2  11416  pfxccatin12lem3  11417  pfxccatin12  11418  pfxccat3  11419  swrdccat  11420  swrdccat3blem  11424  cvg1nlemres  11663  rexanuz  11666  fclim  11972  climmo  11976  iser3shft  12024  fsumsplitsn  12089  fsum2dlemstep  12113  fisumcom2  12117  arisum  12177  arisum2  12178  prodmodc  12257  fprodfac  12294  fprod2dlemstep  12301  fprodcom2fi  12305  fprodsplitsn  12312  eftlub  12369  ef01bndlem  12435  sin01gt0  12441  cos01gt0  12442  sin02gt0  12443  dvdsdivcl  12529  addmodlteqALT  12538  odd2np1  12552  oddge22np1  12560  m1expe  12578  nn0enne  12581  nn0o1gt2  12584  nno  12585  ndvdsadd  12610  dfgcd2  12703  mulgcd  12705  algfx  12742  prmind2  12810  prm2orodd  12816  prmgt1  12822  oddprmgt2  12824  dfphi2  12910  nnnn0modprm0  12946  prm23lt5  12954  pythagtriplem2  12957  pcz  13023  dvdsprmpweqnn  13027  oddprmdvds  13045  prmunb  13053  4sqlem4  13083  4sqlem19  13100  evenennn  13133  fngsum  13590  igsumvalx  13591  dfgrp3me  13802  mulgnn0gsum  13834  rngdi  14073  rngdir  14074  dvdsrcl2  14233  unitinvcl  14257  unitinvinv  14258  unitlinv  14260  unitrinv  14261  rmodislmodlem  14485  rmodislmod  14486  zrhval  14752  psrbagf  14805  distop  14937  ntrss  14971  ssntr  14974  lmrcl  15044  txuni2  15108  txcn  15127  hmeocnvb  15170  xmetunirn  15210  blssioo  15405  divcnap  15417  cdivcncfap  15456  dedekindeulemlub  15472  dedekindicclemlub  15481  dvexp2  15564  elply2  15587  plyco  15611  pilem3  15635  sincosq1sgn  15678  sincosq2sgn  15679  sincosq3sgn  15680  sincosq4sgn  15681  sinq12gt0  15682  fsumdvdsmul  15846  zabsle1  15859  lgsdir2lem4  15891  gausslemma2dlem0f  15914  gausslemma2dlem1a  15918  gausslemma2dlem2  15922  gausslemma2dlem3  15923  gausslemma2dlem4  15924  2lgslem1a1  15946  2lgslem3  15961  2lgsoddprmlem3  15971  2lgsoddprm  15973  2sqlem2  15975  2sqlem10  15985  vtxvalprc  16037  iedgvalprc  16038  upgrex  16085  umgredg  16127  ausgrusgrben  16150  usgruspgrben  16168  usgrislfuspgrdom  16172  uhgr2edg  16188  uspgredg2v  16203  griedg0ssusgr  16233  subusgr  16257  wlkv  16308  wlk1walkdom  16341  trlsv  16366  trlf1  16370  clwwlk1loop  16381  clwwlkext2edg  16404  umgr2cwwkdifex  16407  clwwlknonex2lem2  16420  clwwlknonex2e  16422  eupthv  16428  eupth2lem3lem4fi  16455  konigsberglem5  16474  bj-pm2.18st  16509  bj-dcstab  16515  decidi  16554  sumdc2  16558  bj-charfunbi  16568  bdel  16602  bdssex  16659  bj-indind  16689  findset  16702  nninfall  16774  trirec0  16815  neap0mkv  16841