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  846  notnotrdc  848  condcOLD  859  pm2.61ddc  866  pm5.18dc  888  pm2.25dc  898  pm2.85dc  910  pm5.12dc  915  pm5.14dc  916  pm5.55dc  918  peircedc  919  pm5.54dc  923  dcand  938  dcor  941  pm5.62dc  951  pm5.63dc  952  pm4.83dc  957  ifp2  986  ifpor  993  1fpid3  1000  3simpb  1019  3simpc  1020  3imp  1217  3com12  1231  3com13  1232  syl3anb  1314  xoranor  1419  xorbin  1426  xordc1  1435  biassdc  1437  nfr  1564  nfand  1614  19.21t  1628  19.30dc  1673  exintrbi  1679  19.9t  1688  nfnt  1702  equveli  1805  exdistrfor  1846  sbcof2  1856  sbidm  1897  sbi1v  1938  sbalyz  2050  sbal1yz  2052  nfsb4t  2065  euex  2107  eumo0  2108  mor  2120  exmodc  2128  mo3h  2131  mopick  2156  moexexdc  2162  euexex  2163  2euex  2165  exists2  2175  eqcoms  2232  eleq2s  2324  nfcr  2364  necon3ai  2449  rexnalim  2519  dfrex2dc  2521  rexex  2576  rsp  2577  ralim  2589  rexim  2624  r19.32r  2677  r19.44av  2690  r19.45av  2691  gencl  2832  gencbvex  2847  gencbval  2849  vtoclgf  2859  vtoclg1f  2860  pm13.183  2941  elrabi  2956  eueq2dc  2976  eueq3dc  2977  mob2  2983  euxfr2dc  2988  reu3  2993  rmoim  3004  2rmorex  3009  sbcex  3037  sbcbi2  3079  ra5  3118  sseq1  3247  difdif  3329  dfss4st  3437  difindiss  3458  undif3ss  3465  dfrab3ss  3482  abvor0dc  3515  reldisj  3543  disjel  3546  inssdif0im  3559  uneqdifeqim  3577  r19.2m  3578  r19.2mOLD  3579  r19.3rm  3580  r19.9rmv  3583  rexm  3591  ralm  3595  raaanlem  3596  ifnefalse  3613  ifnotdc  3641  ifandc  3643  ifmdc  3645  nelpri  3690  nelprd  3692  prprc1  3775  difprsn2  3808  diftpsn3  3809  snsssn  3839  preqr2  3847  preq12b  3848  opthpr  3850  prneimg  3852  oprcl  3881  pwprss  3884  intmin4  3951  uniintabim  3960  dfiin2g  3998  iinss2  4018  iundif2ss  4031  disjnim  4073  disjnims  4074  invdisj  4076  disjiun  4078  brne0  4133  brm  4134  trel  4189  trss  4191  ssex  4221  bnd2  4257  abssexg  4266  exmidexmid  4280  rext  4301  unipw  4303  euabex  4311  mss  4312  exss  4313  copsexg  4330  opelopabsb  4348  pwssunim  4375  epelg  4381  sowlin  4411  sotritric  4415  elsuci  4494  sucprc  4503  reusv3  4551  ordon  4578  onsucmin  4599  onsucelsucr  4600  unon  4603  onsucelsucexmid  4622  setind  4631  setind2  4632  sucprcreg  4641  en2lp  4646  eunex  4653  ordsoexmid  4654  ordpwsucss  4659  tfi  4674  peano1  4686  peano2  4687  find  4691  0nelelxp  4748  opelxp  4749  elvvuni  4783  optocl  4795  ralxpf  4868  rexxpf  4869  relop  4872  breldm  4927  reldmm  4942  dmxpm  4944  elreldm  4950  dmrnssfld  4987  dmcosseq  4996  resabs1  5034  resima2  5039  issref  5111  asymref  5114  xpidtr  5119  trin2  5120  poirr2  5121  xpmlem  5149  dmxpss  5159  xp11m  5167  cnveqb  5184  dfco2a  5229  cores2  5241  coi2  5245  relcnvtr  5248  relresfld  5258  relcnvexb  5268  cnviinm  5270  iotauni  5291  iota1  5293  iota4  5298  iotam  5310  dffun8  5346  fununfun  5364  funcnvsn  5366  imadif  5401  imainlem  5402  fcoi1  5508  fcoi2  5509  f0rn0  5522  f1ocnv  5587  f1ocnvb  5588  fun11iun  5595  ffoss  5606  f1o00  5610  fo00  5611  relelfvdm  5661  nfvres  5665  nfunsn  5666  ssimaex  5697  fvmptss2  5711  fvmptssdm  5721  unpreima  5762  respreima  5765  elrnrexdm  5776  elrnrexdmb  5777  rexrnmpt  5780  dffo4  5785  rnmptss  5798  funiun  5818  funopdmsn  5823  fvpr1  5847  fvpr2  5848  elunirn  5896  f1veqaeq  5899  isores1  5944  iotaexel  5965  riotauni  5967  riotacl2  5975  riota1  5980  riota1a  5981  snriota  5992  eusvobj2  5993  acexmidlema  5998  acexmidlemb  5999  acexmidlem2  6004  oprabid  6039  0neqopab  6055  brabvv  6056  1stval2  6307  2ndval2  6308  xp1st  6317  xp2nd  6318  unielxp  6326  releldm2  6337  cnvf1o  6377  fo2ndf  6379  poxp  6384  reldmtpos  6405  dftpos4  6415  tpostpos  6416  tpostpos2  6417  iunon  6436  smoel  6452  tfrlem4  6465  tfrlem7  6469  tfrlem8  6470  tfrlem9  6471  nnaord  6663  ecexr  6693  swoord1  6717  swoord2  6718  0er  6722  mapprc  6807  mapsnconst  6849  ixpf  6875  mptelixpg  6889  idssen  6936  ener  6939  en0  6955  en1  6959  en1bg  6960  2dom  6966  enm  6987  xpsnen  6988  ssenen  7020  snnen2og  7028  php5dom  7032  phpm  7035  findcard  7058  findcard2  7059  findcard2s  7060  unfiexmid  7088  fiintim  7101  fidcenumlemim  7127  sbthlem1  7132  fiss  7152  djuexb  7219  djuss  7245  eldju2ndl  7247  eldju2ndr  7248  ctssdclemr  7287  exmidlpo  7318  finnum  7363  ficardon  7369  exmidfodomrlemim  7387  acnrcl  7391  3nsssucpw1  7429  indpi  7537  subhalfnqq  7609  archnqq  7612  enq0sym  7627  nqnq0pi  7633  nqnq0  7636  mulnnnq0  7645  prml  7672  prmu  7673  prssnql  7674  prssnqu  7675  prcdnql  7679  prcunqu  7680  prltlu  7682  prnmaxl  7683  prnminu  7684  prloc  7686  prdisj  7687  addcanprg  7811  recexprlemopl  7820  recexprlemopu  7822  cauappcvgprlemladdfu  7849  caucvgprlemladdfu  7872  recexgt0sr  7968  renfdisj  8214  axsuploc  8227  negf1o  8536  recexre  8733  apsqgt0  8756  apreim  8758  aprcl  8801  recexaplem2  8807  rerecclap  8885  nn0ge0  9402  elnnnn0b  9421  xnn0xr  9445  xnn0nemnf  9451  xnn0nnn0pnf  9453  znegcl  9485  zeo  9560  nn0ind  9569  nn0ind-raph  9572  uzn0  9746  eluzaddi  9757  eluzsubi  9758  uznn0sub  9762  uz3m2nn  9776  uznnssnn  9780  uz2m1nn  9808  uz2mulcl  9811  indstr2  9812  qmulz  9826  qre  9828  qnegcl  9839  qreccl  9845  rphalflt  9887  nn0ledivnn  9971  xrltnr  9983  nltpnft  10018  ngtmnft  10021  xrrebnd  10023  xnegcl  10036  xnegneg  10037  xltnegi  10039  xrpnfdc  10046  xrmnfdc  10047  xnegid  10063  xaddid1  10066  xnn0lenn0nn0  10069  xnn0xadd0  10071  xposdif  10086  elioore  10116  elfzuz2  10233  uzsubsubfz  10251  fzdisj  10256  fzmmmeqm  10262  elfz0ubfz0  10329  elfz0fzfz0  10330  fz0fzelfz0  10331  fz0fzdiffz0  10334  elfzmlbp  10336  difelfzle  10338  difelfznle  10339  nn0disj  10342  2ffzeq  10345  fzo1fzo0n0  10391  elfzo0z  10392  elfzo0le  10393  fzonmapblen  10395  fzofzim  10396  elfzodifsumelfzo  10415  elfzonlteqm1  10424  fzonn0p1p1  10427  elfzom1p1elfzo  10428  ssfzo12bi  10439  ubmelm1fzo  10440  fzind2  10453  subfzo0  10456  infssuzcldc  10463  rebtwn2z  10482  fldiv4p1lem1div2  10533  fldiv4lem1div2  10535  flqeqceilz  10548  zmodidfzoimp  10584  modfzo0difsn  10625  nnsinds  10675  nn0sinds  10676  expcl2lemap  10781  qexpclz  10790  zzlesq  10938  facp1  10960  facnn2  10964  faclbnd3  10973  bcn1  10988  hashfz0  11055  wrdf  11085  swrdswrdlem  11244  swrdswrd  11245  swrdccatin1  11265  pfxccatin12lem2a  11267  pfxccatin12lem1  11268  swrdccatin2  11269  pfxccatin12lem2  11271  pfxccatin12lem3  11272  pfxccatin12  11273  pfxccat3  11274  swrdccat  11275  swrdccat3blem  11279  cvg1nlemres  11504  rexanuz  11507  fclim  11813  climmo  11817  iser3shft  11865  fsumsplitsn  11929  fsum2dlemstep  11953  fisumcom2  11957  arisum  12017  arisum2  12018  prodmodc  12097  fprodfac  12134  fprod2dlemstep  12141  fprodcom2fi  12145  fprodsplitsn  12152  eftlub  12209  ef01bndlem  12275  sin01gt0  12281  cos01gt0  12282  sin02gt0  12283  dvdsdivcl  12369  addmodlteqALT  12378  odd2np1  12392  oddge22np1  12400  m1expe  12418  nn0enne  12421  nn0o1gt2  12424  nno  12425  ndvdsadd  12450  dfgcd2  12543  mulgcd  12545  algfx  12582  prmind2  12650  prm2orodd  12656  prmgt1  12662  oddprmgt2  12664  dfphi2  12750  nnnn0modprm0  12786  prm23lt5  12794  pythagtriplem2  12797  pcz  12863  dvdsprmpweqnn  12867  oddprmdvds  12885  prmunb  12893  4sqlem4  12923  4sqlem19  12940  evenennn  12972  fngsum  13429  igsumvalx  13430  dfgrp3me  13641  mulgnn0gsum  13673  rngdi  13911  rngdir  13912  dvdsrcl2  14071  unitinvcl  14095  unitinvinv  14096  unitlinv  14098  unitrinv  14099  rmodislmodlem  14322  rmodislmod  14323  zrhval  14589  psrbagf  14642  distop  14767  ntrss  14801  ssntr  14804  lmrcl  14874  txuni2  14938  txcn  14957  hmeocnvb  15000  xmetunirn  15040  blssioo  15235  divcnap  15247  cdivcncfap  15286  dedekindeulemlub  15302  dedekindicclemlub  15311  dvexp2  15394  elply2  15417  plyco  15441  pilem3  15465  sincosq1sgn  15508  sincosq2sgn  15509  sincosq3sgn  15510  sincosq4sgn  15511  sinq12gt0  15512  fsumdvdsmul  15673  zabsle1  15686  lgsdir2lem4  15718  gausslemma2dlem0f  15741  gausslemma2dlem1a  15745  gausslemma2dlem2  15749  gausslemma2dlem3  15750  gausslemma2dlem4  15751  2lgslem1a1  15773  2lgslem3  15788  2lgsoddprmlem3  15798  2lgsoddprm  15800  2sqlem2  15802  2sqlem10  15812  vtxvalprc  15864  iedgvalprc  15865  upgrex  15911  umgredg  15951  ausgrusgrben  15974  usgruspgrben  15992  usgrislfuspgrdom  15996  uhgr2edg  16012  uspgredg2v  16027  wlkv  16047  wlk1walkdom  16080  trlsv  16103  trlf1  16106  bj-pm2.18st  16138  bj-dcstab  16144  decidi  16183  sumdc2  16187  bj-charfunbi  16198  bdel  16232  bdssex  16289  bj-indind  16319  findset  16332  nninfall  16405  trirec0  16442  neap0mkv  16467