Theorem sylbi 120

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 119	. 2 ⊢ (𝜑 → 𝜓)
3		sylbi.2	. 2 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbb  122  sylbb2  137  3imtr4i  200  simplbiim  385  mpan10  466  an12s  555  an32s  558  an4s  578  sylnbi  668  dcim  831  notnotrdc  833  condcOLD  844  pm2.61ddc  851  pm5.18dc  873  pm2.25dc  883  pm2.85dc  895  pm5.12dc  900  pm5.14dc  901  pm5.55dc  903  peircedc  904  pm5.54dc  908  dcor  925  pm5.62dc  935  pm5.63dc  936  pm4.83dc  941  3simpb  985  3simpc  986  3imp  1183  3com12  1197  3com13  1198  syl3anb  1271  xoranor  1367  xorbin  1374  xordc1  1383  biassdc  1385  nfr  1506  nfand  1556  19.21t  1570  19.30dc  1615  exintrbi  1621  19.9t  1630  nfnt  1644  equveli  1747  exdistrfor  1788  sbcof2  1798  sbidm  1839  sbi1v  1879  sbalyz  1987  sbal1yz  1989  nfsb4t  2002  euex  2044  eumo0  2045  mor  2056  exmodc  2064  mo3h  2067  mopick  2092  moexexdc  2098  euexex  2099  2euex  2101  exists2  2111  eqcoms  2168  eleq2s  2261  nfcr  2300  necon3ai  2385  rexnalim  2455  dfrex2dc  2457  rexex  2512  rsp  2513  ralim  2525  rexim  2560  r19.32r  2612  r19.44av  2625  r19.45av  2626  gencl  2758  gencbvex  2772  gencbval  2774  vtoclgf  2784  vtoclg1f  2785  pm13.183  2864  elrabi  2879  eueq2dc  2899  eueq3dc  2900  mob2  2906  euxfr2dc  2911  reu3  2916  rmoim  2927  2rmorex  2932  sbcex  2959  sbcbi2  3001  ra5  3039  sseq1  3165  difdif  3247  dfss4st  3355  difindiss  3376  undif3ss  3383  dfrab3ss  3400  abvor0dc  3432  reldisj  3460  disjel  3463  inssdif0im  3476  uneqdifeqim  3494  r19.2m  3495  r19.2mOLD  3496  r19.3rm  3497  r19.9rmv  3500  rexm  3508  ralm  3513  raaanlem  3514  ifnefalse  3531  ifnotdc  3556  ifandc  3557  ifmdc  3558  nelpri  3600  nelprd  3602  prprc1  3684  difprsn2  3713  diftpsn3  3714  snsssn  3741  preqr2  3749  preq12b  3750  opthpr  3752  prneimg  3754  oprcl  3782  pwprss  3785  intmin4  3852  uniintabim  3861  dfiin2g  3899  iinss2  3918  iundif2ss  3931  disjnim  3973  disjnims  3974  invdisj  3976  disjiun  3977  brne0  4031  brm  4032  trel  4087  trss  4089  ssex  4119  bnd2  4152  abssexg  4161  exmidexmid  4175  rext  4193  unipw  4195  euabex  4203  mss  4204  exss  4205  copsexg  4222  opelopabsb  4238  pwssunim  4262  epelg  4268  sowlin  4298  sotritric  4302  elsuci  4381  sucprc  4390  reusv3  4438  ordon  4463  onsucmin  4484  onsucelsucr  4485  unon  4488  onsucelsucexmid  4507  setind  4516  setind2  4517  sucprcreg  4526  en2lp  4531  eunex  4538  ordsoexmid  4539  ordpwsucss  4544  tfi  4559  peano1  4571  peano2  4572  find  4576  0nelelxp  4633  opelxp  4634  elvvuni  4668  optocl  4680  ralxpf  4750  rexxpf  4751  relop  4754  breldm  4808  dmxpm  4824  elreldm  4830  dmrnssfld  4867  dmcosseq  4875  resabs1  4913  resima2  4918  issref  4986  asymref  4989  xpidtr  4994  trin2  4995  poirr2  4996  xpmlem  5024  dmxpss  5034  xp11m  5042  cnveqb  5059  dfco2a  5104  cores2  5116  coi2  5120  relcnvtr  5123  relresfld  5133  relcnvexb  5143  cnviinm  5145  iotauni  5165  iota1  5167  iota4  5171  dffun8  5216  funcnvsn  5233  imadif  5268  imainlem  5269  fcoi1  5368  fcoi2  5369  f0rn0  5382  f1ocnv  5445  f1ocnvb  5446  fun11iun  5453  ffoss  5464  f1o00  5467  fo00  5468  relelfvdm  5518  nfvres  5519  nfunsn  5520  ssimaex  5547  fvmptss2  5561  fvmptssdm  5570  unpreima  5610  respreima  5613  elrnrexdm  5624  elrnrexdmb  5625  rexrnmpt  5628  dffo4  5633  rnmptss  5646  fvpr1  5689  fvpr2  5690  elunirn  5734  f1veqaeq  5737  isores1  5782  riotauni  5804  riotacl2  5811  riota1  5816  riota1a  5817  snriota  5827  eusvobj2  5828  acexmidlema  5833  acexmidlemb  5834  acexmidlem2  5839  oprabid  5874  0neqopab  5887  brabvv  5888  1stval2  6123  2ndval2  6124  xp1st  6133  xp2nd  6134  unielxp  6142  releldm2  6153  cnvf1o  6193  fo2ndf  6195  poxp  6200  reldmtpos  6221  dftpos4  6231  tpostpos  6232  tpostpos2  6233  iunon  6252  smoel  6268  tfrlem4  6281  tfrlem7  6285  tfrlem8  6286  tfrlem9  6287  nnaord  6477  ecexr  6506  swoord1  6530  swoord2  6531  0er  6535  mapprc  6618  mapsnconst  6660  ixpf  6686  mptelixpg  6700  idssen  6743  ener  6745  en0  6761  en1  6765  en1bg  6766  2dom  6771  enm  6786  xpsnen  6787  ssenen  6817  snnen2og  6825  php5dom  6829  phpm  6831  findcard  6854  findcard2  6855  findcard2s  6856  unfiexmid  6883  fiintim  6894  fidcenumlemim  6917  sbthlem1  6922  fiss  6942  djuexb  7009  djuss  7035  eldju2ndl  7037  eldju2ndr  7038  ctssdclemr  7077  exmidlpo  7107  finnum  7139  exmidfodomrlemim  7157  3nsssucpw1  7192  indpi  7283  subhalfnqq  7355  archnqq  7358  enq0sym  7373  nqnq0pi  7379  nqnq0  7382  mulnnnq0  7391  prml  7418  prmu  7419  prssnql  7420  prssnqu  7421  prcdnql  7425  prcunqu  7426  prltlu  7428  prnmaxl  7429  prnminu  7430  prloc  7432  prdisj  7433  addcanprg  7557  recexprlemopl  7566  recexprlemopu  7568  cauappcvgprlemladdfu  7595  caucvgprlemladdfu  7618  recexgt0sr  7714  renfdisj  7958  axsuploc  7971  negf1o  8280  recexre  8476  apsqgt0  8499  apreim  8501  aprcl  8544  recexaplem2  8549  rerecclap  8626  nn0ge0  9139  elnnnn0b  9158  xnn0xr  9182  xnn0nemnf  9188  xnn0nnn0pnf  9190  znegcl  9222  zeo  9296  nn0ind  9305  nn0ind-raph  9308  uzn0  9481  eluzaddi  9492  eluzsubi  9493  uznn0sub  9497  uz3m2nn  9511  uznnssnn  9515  uz2m1nn  9543  uz2mulcl  9546  indstr2  9547  qmulz  9561  qre  9563  qnegcl  9574  qreccl  9580  rphalflt  9619  nn0ledivnn  9703  xrltnr  9715  nltpnft  9750  ngtmnft  9753  xrrebnd  9755  xnegcl  9768  xnegneg  9769  xltnegi  9771  xrpnfdc  9778  xrmnfdc  9779  xnegid  9795  xaddid1  9798  xnn0lenn0nn0  9801  xnn0xadd0  9803  xposdif  9818  elioore  9848  elfzuz2  9964  uzsubsubfz  9982  fzdisj  9987  fzmmmeqm  9993  elfz0ubfz0  10060  elfz0fzfz0  10061  fz0fzelfz0  10062  fz0fzdiffz0  10065  elfzmlbp  10067  difelfzle  10069  difelfznle  10070  nn0disj  10073  2ffzeq  10076  fzo1fzo0n0  10118  elfzo0z  10119  elfzo0le  10120  fzonmapblen  10122  fzofzim  10123  elfzodifsumelfzo  10136  elfzonlteqm1  10145  fzonn0p1p1  10148  elfzom1p1elfzo  10149  ssfzo12bi  10160  ubmelm1fzo  10161  fzind2  10174  subfzo0  10177  rebtwn2z  10190  fldiv4p1lem1div2  10240  flqeqceilz  10253  zmodidfzoimp  10289  modfzo0difsn  10330  nnsinds  10378  nn0sinds  10379  expcl2lemap  10467  qexpclz  10476  facp1  10643  facnn2  10647  faclbnd3  10656  bcn1  10671  hashfz0  10738  cvg1nlemres  10927  rexanuz  10930  fclim  11235  climmo  11239  iser3shft  11287  fsumsplitsn  11351  fsum2dlemstep  11375  fisumcom2  11379  arisum  11439  arisum2  11440  prodmodc  11519  fprodfac  11556  fprod2dlemstep  11563  fprodcom2fi  11567  fprodsplitsn  11574  eftlub  11631  ef01bndlem  11697  sin01gt0  11702  cos01gt0  11703  sin02gt0  11704  dvdsdivcl  11788  addmodlteqALT  11797  odd2np1  11810  oddge22np1  11818  m1expe  11836  nn0enne  11839  nn0o1gt2  11842  nno  11843  ndvdsadd  11868  infssuzcldc  11884  dfgcd2  11947  mulgcd  11949  algfx  11984  prmind2  12052  prm2orodd  12058  prmgt1  12064  oddprmgt2  12066  dfphi2  12152  nnnn0modprm0  12187  prm23lt5  12195  pythagtriplem2  12198  pcz  12263  dvdsprmpweqnn  12267  oddprmdvds  12284  prmunb  12292  4sqlem4  12322  evenennn  12326  distop  12735  ntrss  12769  ssntr  12772  lmrcl  12841  lmreltop  12843  txuni2  12906  txcn  12925  hmeocnvb  12968  xmetunirn  13008  blssioo  13195  divcnap  13205  cdivcncfap  13237  dedekindeulemlub  13248  dedekindicclemlub  13257  dvexp2  13326  pilem3  13354  sincosq1sgn  13397  sincosq2sgn  13398  sincosq3sgn  13399  sincosq4sgn  13400  sinq12gt0  13401  zabsle1  13550  lgsdir2lem4  13582  2sqlem2  13601  2sqlem10  13611  bj-pm2.18st  13641  bj-dcstab  13647  decidi  13686  sumdc2  13690  bj-charfunbi  13703  bdel  13737  bdssex  13794  bj-indind  13824  findset  13837  nninfall  13899  trirec0  13933