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  2833  gencbvex  2848  gencbval  2850  vtoclgf  2860  vtoclg1f  2861  pm13.183  2942  elrabi  2957  eueq2dc  2977  eueq3dc  2978  mob2  2984  euxfr2dc  2989  reu3  2994  rmoim  3005  2rmorex  3010  sbcex  3038  sbcbi2  3080  ra5  3119  sseq1  3248  difdif  3330  dfss4st  3438  difindiss  3459  undif3ss  3466  dfrab3ss  3483  abvor0dc  3516  reldisj  3544  disjel  3547  inssdif0im  3560  uneqdifeqim  3578  r19.2m  3579  r19.2mOLD  3580  r19.3rm  3581  r19.9rmv  3584  rexm  3592  ralm  3596  raaanlem  3597  ifnefalse  3614  ifnotdc  3642  ifandc  3644  ifmdc  3646  nelpri  3691  nelprd  3693  prprc1  3778  difprsn2  3811  diftpsn3  3812  snsssn  3842  preqr2  3850  preq12b  3851  opthpr  3853  prneimg  3855  oprcl  3884  pwprss  3887  intmin4  3954  uniintabim  3963  dfiin2g  4001  iinss2  4021  iundif2ss  4034  disjnim  4076  disjnims  4077  invdisj  4079  disjiun  4081  brne0  4136  brm  4137  trel  4192  trss  4194  ssex  4224  bnd2  4261  abssexg  4270  exmidexmid  4284  rext  4305  unipw  4307  euabex  4315  mss  4316  exss  4317  copsexg  4334  opelopabsb  4352  pwssunim  4379  epelg  4385  sowlin  4415  sotritric  4419  elsuci  4498  sucprc  4507  reusv3  4555  ordon  4582  onsucmin  4603  onsucelsucr  4604  unon  4607  onsucelsucexmid  4626  setind  4635  setind2  4636  sucprcreg  4645  en2lp  4650  eunex  4657  ordsoexmid  4658  ordpwsucss  4663  tfi  4678  peano1  4690  peano2  4691  find  4695  0nelelxp  4752  opelxp  4753  elvvuni  4788  optocl  4800  ralxpf  4874  rexxpf  4875  relop  4878  breldm  4933  reldmm  4948  dmxpm  4950  elreldm  4956  dmrnssfld  4993  dmcosseq  5002  resabs1  5040  resima2  5045  issref  5117  asymref  5120  xpidtr  5125  trin2  5126  poirr2  5127  xpmlem  5155  dmxpss  5165  xp11m  5173  cnveqb  5190  dfco2a  5235  cores2  5247  coi2  5251  relcnvtr  5254  relresfld  5264  relcnvexb  5274  cnviinm  5276  iotauni  5297  iota1  5299  iota4  5304  iotam  5316  dffun8  5352  fununfun  5370  funcnvsn  5372  imadif  5407  imainlem  5408  fcoi1  5514  fcoi2  5515  f0rn0  5528  f1ocnv  5593  f1ocnvb  5594  fun11iun  5601  ffoss  5612  f1o00  5616  fo00  5617  relelfvdm  5667  nfvres  5671  nfunsn  5672  ssimaex  5703  fvmptss2  5717  fvmptssdm  5727  unpreima  5768  respreima  5771  elrnrexdm  5782  elrnrexdmb  5783  rexrnmpt  5786  dffo4  5791  rnmptss  5804  funiun  5824  funopdmsn  5829  fvpr1  5853  fvpr2  5854  elunirn  5902  f1veqaeq  5905  isores1  5950  iotaexel  5971  riotauni  5973  riotacl2  5981  riota1  5986  riota1a  5987  snriota  5998  eusvobj2  5999  acexmidlema  6004  acexmidlemb  6005  acexmidlem2  6010  oprabid  6045  0neqopab  6061  brabvv  6062  1stval2  6313  2ndval2  6314  xp1st  6323  xp2nd  6324  unielxp  6332  releldm2  6343  cnvf1o  6385  fo2ndf  6387  poxp  6392  reldmtpos  6414  dftpos4  6424  tpostpos  6425  tpostpos2  6426  iunon  6445  smoel  6461  tfrlem4  6474  tfrlem7  6478  tfrlem8  6479  tfrlem9  6480  nnaord  6672  ecexr  6702  swoord1  6726  swoord2  6727  0er  6731  mapprc  6816  mapsnconst  6858  ixpf  6884  mptelixpg  6898  idssen  6945  ener  6948  en0  6964  en1  6968  en1bg  6969  2dom  6975  modom  6989  enm  6999  xpsnen  7000  ssenen  7032  snnen2og  7040  php5dom  7044  phpm  7047  findcard  7072  findcard2  7073  findcard2s  7074  unfiexmid  7105  fiintim  7118  fidcenumlemim  7145  sbthlem1  7150  fiss  7170  djuexb  7237  djuss  7263  eldju2ndl  7265  eldju2ndr  7266  ctssdclemr  7305  exmidlpo  7336  finnum  7381  ficardon  7387  exmidfodomrlemim  7405  acnrcl  7409  3nsssucpw1  7447  indpi  7555  subhalfnqq  7627  archnqq  7630  enq0sym  7645  nqnq0pi  7651  nqnq0  7654  mulnnnq0  7663  prml  7690  prmu  7691  prssnql  7692  prssnqu  7693  prcdnql  7697  prcunqu  7698  prltlu  7700  prnmaxl  7701  prnminu  7702  prloc  7704  prdisj  7705  addcanprg  7829  recexprlemopl  7838  recexprlemopu  7840  cauappcvgprlemladdfu  7867  caucvgprlemladdfu  7890  recexgt0sr  7986  renfdisj  8232  axsuploc  8245  negf1o  8554  recexre  8751  apsqgt0  8774  apreim  8776  aprcl  8819  recexaplem2  8825  rerecclap  8903  nn0ge0  9420  elnnnn0b  9439  xnn0xr  9463  xnn0nemnf  9469  xnn0nnn0pnf  9471  znegcl  9503  zeo  9578  nn0ind  9587  nn0ind-raph  9590  uzn0  9765  eluzaddi  9776  eluzsubi  9777  uznn0sub  9781  uz3m2nn  9800  uznnssnn  9804  uz2m1nn  9832  uz2mulcl  9835  indstr2  9836  qmulz  9850  qre  9852  qnegcl  9863  qreccl  9869  rphalflt  9911  nn0ledivnn  9995  xrltnr  10007  nltpnft  10042  ngtmnft  10045  xrrebnd  10047  xnegcl  10060  xnegneg  10061  xltnegi  10063  xrpnfdc  10070  xrmnfdc  10071  xnegid  10087  xaddid1  10090  xnn0lenn0nn0  10093  xnn0xadd0  10095  xposdif  10110  elioore  10140  elfzuz2  10257  uzsubsubfz  10275  fzdisj  10280  fzmmmeqm  10286  elfz0ubfz0  10353  elfz0fzfz0  10354  fz0fzelfz0  10355  fz0fzdiffz0  10358  elfzmlbp  10360  difelfzle  10362  difelfznle  10363  nn0disj  10366  2ffzeq  10369  fzo1fzo0n0  10415  elfzo0z  10416  elfzo0le  10417  fzonmapblen  10419  fzofzim  10420  elfzodifsumelfzo  10439  elfzonlteqm1  10448  fzonn0p1p1  10451  elfzom1p1elfzo  10452  ssfzo12bi  10463  ubmelm1fzo  10464  fzind2  10478  subfzo0  10481  infssuzcldc  10488  rebtwn2z  10507  fldiv4p1lem1div2  10558  fldiv4lem1div2  10560  flqeqceilz  10573  zmodidfzoimp  10609  modfzo0difsn  10650  nnsinds  10700  nn0sinds  10701  expcl2lemap  10806  qexpclz  10815  zzlesq  10963  facp1  10985  facnn2  10989  faclbnd3  10998  bcn1  11013  hashfz0  11082  wrdf  11112  swrdswrdlem  11278  swrdswrd  11279  swrdccatin1  11299  pfxccatin12lem2a  11301  pfxccatin12lem1  11302  swrdccatin2  11303  pfxccatin12lem2  11305  pfxccatin12lem3  11306  pfxccatin12  11307  pfxccat3  11308  swrdccat  11309  swrdccat3blem  11313  cvg1nlemres  11539  rexanuz  11542  fclim  11848  climmo  11852  iser3shft  11900  fsumsplitsn  11964  fsum2dlemstep  11988  fisumcom2  11992  arisum  12052  arisum2  12053  prodmodc  12132  fprodfac  12169  fprod2dlemstep  12176  fprodcom2fi  12180  fprodsplitsn  12187  eftlub  12244  ef01bndlem  12310  sin01gt0  12316  cos01gt0  12317  sin02gt0  12318  dvdsdivcl  12404  addmodlteqALT  12413  odd2np1  12427  oddge22np1  12435  m1expe  12453  nn0enne  12456  nn0o1gt2  12459  nno  12460  ndvdsadd  12485  dfgcd2  12578  mulgcd  12580  algfx  12617  prmind2  12685  prm2orodd  12691  prmgt1  12697  oddprmgt2  12699  dfphi2  12785  nnnn0modprm0  12821  prm23lt5  12829  pythagtriplem2  12832  pcz  12898  dvdsprmpweqnn  12902  oddprmdvds  12920  prmunb  12928  4sqlem4  12958  4sqlem19  12975  evenennn  13007  fngsum  13464  igsumvalx  13465  dfgrp3me  13676  mulgnn0gsum  13708  rngdi  13946  rngdir  13947  dvdsrcl2  14106  unitinvcl  14130  unitinvinv  14131  unitlinv  14133  unitrinv  14134  rmodislmodlem  14357  rmodislmod  14358  zrhval  14624  psrbagf  14677  distop  14802  ntrss  14836  ssntr  14839  lmrcl  14909  txuni2  14973  txcn  14992  hmeocnvb  15035  xmetunirn  15075  blssioo  15270  divcnap  15282  cdivcncfap  15321  dedekindeulemlub  15337  dedekindicclemlub  15346  dvexp2  15429  elply2  15452  plyco  15476  pilem3  15500  sincosq1sgn  15543  sincosq2sgn  15544  sincosq3sgn  15545  sincosq4sgn  15546  sinq12gt0  15547  fsumdvdsmul  15708  zabsle1  15721  lgsdir2lem4  15753  gausslemma2dlem0f  15776  gausslemma2dlem1a  15780  gausslemma2dlem2  15784  gausslemma2dlem3  15785  gausslemma2dlem4  15786  2lgslem1a1  15808  2lgslem3  15823  2lgsoddprmlem3  15833  2lgsoddprm  15835  2sqlem2  15837  2sqlem10  15847  vtxvalprc  15899  iedgvalprc  15900  upgrex  15947  umgredg  15989  ausgrusgrben  16012  usgruspgrben  16030  usgrislfuspgrdom  16034  uhgr2edg  16050  uspgredg2v  16065  griedg0ssusgr  16095  wlkv  16137  wlk1walkdom  16170  trlsv  16193  trlf1  16197  clwwlk1loop  16208  clwwlkext2edg  16231  umgr2cwwkdifex  16234  clwwlknonex2lem2  16247  clwwlknonex2e  16249  eupthv  16255  bj-pm2.18st  16296  bj-dcstab  16302  decidi  16341  sumdc2  16345  bj-charfunbi  16356  bdel  16390  bdssex  16447  bj-indind  16477  findset  16490  nninfall  16561  trirec0  16598  neap0mkv  16623