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  4258  abssexg  4267  exmidexmid  4281  rext  4302  unipw  4304  euabex  4312  mss  4313  exss  4314  copsexg  4331  opelopabsb  4349  pwssunim  4376  epelg  4382  sowlin  4412  sotritric  4416  elsuci  4495  sucprc  4504  reusv3  4552  ordon  4579  onsucmin  4600  onsucelsucr  4601  unon  4604  onsucelsucexmid  4623  setind  4632  setind2  4633  sucprcreg  4642  en2lp  4647  eunex  4654  ordsoexmid  4655  ordpwsucss  4660  tfi  4675  peano1  4687  peano2  4688  find  4692  0nelelxp  4749  opelxp  4750  elvvuni  4785  optocl  4797  ralxpf  4871  rexxpf  4872  relop  4875  breldm  4930  reldmm  4945  dmxpm  4947  elreldm  4953  dmrnssfld  4990  dmcosseq  4999  resabs1  5037  resima2  5042  issref  5114  asymref  5117  xpidtr  5122  trin2  5123  poirr2  5124  xpmlem  5152  dmxpss  5162  xp11m  5170  cnveqb  5187  dfco2a  5232  cores2  5244  coi2  5248  relcnvtr  5251  relresfld  5261  relcnvexb  5271  cnviinm  5273  iotauni  5294  iota1  5296  iota4  5301  iotam  5313  dffun8  5349  fununfun  5367  funcnvsn  5369  imadif  5404  imainlem  5405  fcoi1  5511  fcoi2  5512  f0rn0  5525  f1ocnv  5590  f1ocnvb  5591  fun11iun  5598  ffoss  5609  f1o00  5613  fo00  5614  relelfvdm  5664  nfvres  5668  nfunsn  5669  ssimaex  5700  fvmptss2  5714  fvmptssdm  5724  unpreima  5765  respreima  5768  elrnrexdm  5779  elrnrexdmb  5780  rexrnmpt  5783  dffo4  5788  rnmptss  5801  funiun  5821  funopdmsn  5826  fvpr1  5850  fvpr2  5851  elunirn  5899  f1veqaeq  5902  isores1  5947  iotaexel  5968  riotauni  5970  riotacl2  5978  riota1  5983  riota1a  5984  snriota  5995  eusvobj2  5996  acexmidlema  6001  acexmidlemb  6002  acexmidlem2  6007  oprabid  6042  0neqopab  6058  brabvv  6059  1stval2  6310  2ndval2  6311  xp1st  6320  xp2nd  6321  unielxp  6329  releldm2  6340  cnvf1o  6382  fo2ndf  6384  poxp  6389  reldmtpos  6410  dftpos4  6420  tpostpos  6421  tpostpos2  6422  iunon  6441  smoel  6457  tfrlem4  6470  tfrlem7  6474  tfrlem8  6475  tfrlem9  6476  nnaord  6668  ecexr  6698  swoord1  6722  swoord2  6723  0er  6727  mapprc  6812  mapsnconst  6854  ixpf  6880  mptelixpg  6894  idssen  6941  ener  6944  en0  6960  en1  6964  en1bg  6965  2dom  6971  enm  6992  xpsnen  6993  ssenen  7025  snnen2og  7033  php5dom  7037  phpm  7040  findcard  7063  findcard2  7064  findcard2s  7065  unfiexmid  7096  fiintim  7109  fidcenumlemim  7135  sbthlem1  7140  fiss  7160  djuexb  7227  djuss  7253  eldju2ndl  7255  eldju2ndr  7256  ctssdclemr  7295  exmidlpo  7326  finnum  7371  ficardon  7377  exmidfodomrlemim  7395  acnrcl  7399  3nsssucpw1  7437  indpi  7545  subhalfnqq  7617  archnqq  7620  enq0sym  7635  nqnq0pi  7641  nqnq0  7644  mulnnnq0  7653  prml  7680  prmu  7681  prssnql  7682  prssnqu  7683  prcdnql  7687  prcunqu  7688  prltlu  7690  prnmaxl  7691  prnminu  7692  prloc  7694  prdisj  7695  addcanprg  7819  recexprlemopl  7828  recexprlemopu  7830  cauappcvgprlemladdfu  7857  caucvgprlemladdfu  7880  recexgt0sr  7976  renfdisj  8222  axsuploc  8235  negf1o  8544  recexre  8741  apsqgt0  8764  apreim  8766  aprcl  8809  recexaplem2  8815  rerecclap  8893  nn0ge0  9410  elnnnn0b  9429  xnn0xr  9453  xnn0nemnf  9459  xnn0nnn0pnf  9461  znegcl  9493  zeo  9568  nn0ind  9577  nn0ind-raph  9580  uzn0  9755  eluzaddi  9766  eluzsubi  9767  uznn0sub  9771  uz3m2nn  9785  uznnssnn  9789  uz2m1nn  9817  uz2mulcl  9820  indstr2  9821  qmulz  9835  qre  9837  qnegcl  9848  qreccl  9854  rphalflt  9896  nn0ledivnn  9980  xrltnr  9992  nltpnft  10027  ngtmnft  10030  xrrebnd  10032  xnegcl  10045  xnegneg  10046  xltnegi  10048  xrpnfdc  10055  xrmnfdc  10056  xnegid  10072  xaddid1  10075  xnn0lenn0nn0  10078  xnn0xadd0  10080  xposdif  10095  elioore  10125  elfzuz2  10242  uzsubsubfz  10260  fzdisj  10265  fzmmmeqm  10271  elfz0ubfz0  10338  elfz0fzfz0  10339  fz0fzelfz0  10340  fz0fzdiffz0  10343  elfzmlbp  10345  difelfzle  10347  difelfznle  10348  nn0disj  10351  2ffzeq  10354  fzo1fzo0n0  10400  elfzo0z  10401  elfzo0le  10402  fzonmapblen  10404  fzofzim  10405  elfzodifsumelfzo  10424  elfzonlteqm1  10433  fzonn0p1p1  10436  elfzom1p1elfzo  10437  ssfzo12bi  10448  ubmelm1fzo  10449  fzind2  10462  subfzo0  10465  infssuzcldc  10472  rebtwn2z  10491  fldiv4p1lem1div2  10542  fldiv4lem1div2  10544  flqeqceilz  10557  zmodidfzoimp  10593  modfzo0difsn  10634  nnsinds  10684  nn0sinds  10685  expcl2lemap  10790  qexpclz  10799  zzlesq  10947  facp1  10969  facnn2  10973  faclbnd3  10982  bcn1  10997  hashfz0  11065  wrdf  11095  swrdswrdlem  11257  swrdswrd  11258  swrdccatin1  11278  pfxccatin12lem2a  11280  pfxccatin12lem1  11281  swrdccatin2  11282  pfxccatin12lem2  11284  pfxccatin12lem3  11285  pfxccatin12  11286  pfxccat3  11287  swrdccat  11288  swrdccat3blem  11292  cvg1nlemres  11517  rexanuz  11520  fclim  11826  climmo  11830  iser3shft  11878  fsumsplitsn  11942  fsum2dlemstep  11966  fisumcom2  11970  arisum  12030  arisum2  12031  prodmodc  12110  fprodfac  12147  fprod2dlemstep  12154  fprodcom2fi  12158  fprodsplitsn  12165  eftlub  12222  ef01bndlem  12288  sin01gt0  12294  cos01gt0  12295  sin02gt0  12296  dvdsdivcl  12382  addmodlteqALT  12391  odd2np1  12405  oddge22np1  12413  m1expe  12431  nn0enne  12434  nn0o1gt2  12437  nno  12438  ndvdsadd  12463  dfgcd2  12556  mulgcd  12558  algfx  12595  prmind2  12663  prm2orodd  12669  prmgt1  12675  oddprmgt2  12677  dfphi2  12763  nnnn0modprm0  12799  prm23lt5  12807  pythagtriplem2  12810  pcz  12876  dvdsprmpweqnn  12880  oddprmdvds  12898  prmunb  12906  4sqlem4  12936  4sqlem19  12953  evenennn  12985  fngsum  13442  igsumvalx  13443  dfgrp3me  13654  mulgnn0gsum  13686  rngdi  13924  rngdir  13925  dvdsrcl2  14084  unitinvcl  14108  unitinvinv  14109  unitlinv  14111  unitrinv  14112  rmodislmodlem  14335  rmodislmod  14336  zrhval  14602  psrbagf  14655  distop  14780  ntrss  14814  ssntr  14817  lmrcl  14887  txuni2  14951  txcn  14970  hmeocnvb  15013  xmetunirn  15053  blssioo  15248  divcnap  15260  cdivcncfap  15299  dedekindeulemlub  15315  dedekindicclemlub  15324  dvexp2  15407  elply2  15430  plyco  15454  pilem3  15478  sincosq1sgn  15521  sincosq2sgn  15522  sincosq3sgn  15523  sincosq4sgn  15524  sinq12gt0  15525  fsumdvdsmul  15686  zabsle1  15699  lgsdir2lem4  15731  gausslemma2dlem0f  15754  gausslemma2dlem1a  15758  gausslemma2dlem2  15762  gausslemma2dlem3  15763  gausslemma2dlem4  15764  2lgslem1a1  15786  2lgslem3  15801  2lgsoddprmlem3  15811  2lgsoddprm  15813  2sqlem2  15815  2sqlem10  15825  vtxvalprc  15877  iedgvalprc  15878  upgrex  15924  umgredg  15964  ausgrusgrben  15987  usgruspgrben  16005  usgrislfuspgrdom  16009  uhgr2edg  16025  uspgredg2v  16040  griedg0ssusgr  16070  wlkv  16098  wlk1walkdom  16131  trlsv  16154  trlf1  16157  clwwlk1loop  16168  clwwlkext2edg  16190  umgr2cwwkdifex  16193  bj-pm2.18st  16223  bj-dcstab  16229  decidi  16268  sumdc2  16272  bj-charfunbi  16283  bdel  16317  bdssex  16374  bj-indind  16404  findset  16417  nninfall  16489  trirec0  16526  neap0mkv  16551