Theorem sylbi 119

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

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sylbb  121  sylbb2  136  3imtr4i  199  simplbiim  379  mpan10  458  an12s  530  an32s  533  an4s  553  sylnbi  636  condc  783  notnotrdc  785  pm2.61ddc  792  pm5.18dc  811  dcim  818  pm2.25dc  826  pm2.85dc  845  pm5.12dc  850  pm5.14dc  851  pm5.55dc  853  peircedc  854  pm5.54dc  861  dcor  877  pm5.62dc  887  pm5.63dc  888  pm4.83dc  893  3simpb  937  3simpc  938  3imp  1133  3com12  1143  3com13  1144  syl3anb  1213  xoranor  1309  xorbin  1316  xordc1  1325  biassdc  1327  nfr  1452  nfand  1501  19.21t  1515  19.30dc  1559  exintrbi  1565  19.9t  1574  nfnt  1587  equveli  1684  exdistrfor  1723  sbcof2  1733  sbidm  1774  sbi1v  1814  sbalyz  1918  sbal1yz  1920  nfsb4t  1933  euex  1973  eumo0  1974  mor  1985  exmodc  1993  mo3h  1996  mopick  2021  moexexdc  2027  euexex  2028  2euex  2030  exists2  2040  eqcoms  2086  eleq2s  2177  nfcr  2215  necon3ai  2298  rexnalim  2364  dfrex2dc  2365  rexex  2416  rsp  2417  ralim  2428  rexim  2461  r19.32r  2507  r19.44av  2519  r19.45av  2520  gencl  2642  gencbvex  2656  gencbval  2658  vtoclgf  2668  pm13.183  2742  elrabi  2756  eueq2dc  2776  eueq3dc  2777  mob2  2783  euxfr2dc  2788  reu3  2793  rmoim  2802  2rmorex  2807  sbcex  2834  sbcbi2  2875  ra5  2913  sseq1  3031  difdif  3109  difindiss  3236  undif3ss  3243  dfrab3ss  3260  abvor0dc  3289  reldisj  3316  disjel  3319  inssdif0im  3332  uneqdifeqim  3349  r19.2m  3350  r19.3rm  3351  r19.9rmv  3354  rexm  3362  ralm  3367  raaanlem  3368  ifnefalse  3384  nelpri  3446  prprc1  3524  difprsn2  3551  diftpsn3  3552  snsssn  3579  preqr2  3587  preq12b  3588  opthpr  3590  prneimg  3592  oprcl  3620  pwprss  3623  intmin4  3690  uniintabim  3699  dfiin2g  3737  iinss2  3756  iundif2ss  3769  invdisj  3806  trel  3908  trss  3910  ssex  3941  bnd2  3973  abssexg  3981  exmidexmid  3995  rext  4006  unipw  4008  euabex  4016  mss  4017  exss  4018  copsexg  4035  opelopabsb  4051  pwssunim  4075  epelg  4081  sowlin  4111  sotritric  4115  elsuci  4194  sucprc  4203  reusv3  4246  ordon  4266  onsucmin  4287  onsucelsucr  4288  unon  4291  onsucelsucexmid  4309  setind  4318  setind2  4319  sucprcreg  4328  en2lp  4333  eunex  4340  ordsoexmid  4341  ordpwsucss  4346  tfi  4360  peano1  4372  peano2  4373  find  4377  0nelelxp  4429  opelxp  4430  elvvuni  4460  optocl  4472  ralxpf  4540  rexxpf  4541  relop  4544  breldm  4598  dmxpm  4614  elreldm  4619  dmrnssfld  4654  dmcosseq  4662  resabs1  4699  resima2  4703  issref  4769  asymref  4772  xpidtr  4777  trin2  4778  poirr2  4779  xpmlem  4806  dmxpss  4815  xp11m  4823  cnveqb  4840  dfco2a  4885  cores2  4897  coi2  4901  relcnvtr  4904  relresfld  4914  relcnvexb  4924  cnviinm  4926  iotauni  4946  iota1  4948  iota4  4952  dffun8  4996  funcnvsn  5012  imadif  5047  imainlem  5048  fcoi1  5139  fcoi2  5140  f0rn0  5153  f1ocnv  5214  f1ocnvb  5215  fun11iun  5222  ffoss  5233  f1o00  5236  fo00  5237  relelfvdm  5281  nfvres  5282  nfunsn  5283  ssimaex  5310  fvmptss2  5324  fvmptssdm  5332  unpreima  5369  respreima  5372  elrnrexdm  5383  elrnrexdmb  5384  rexrnmpt  5387  dffo4  5392  rnmptss  5401  fvpr1  5441  fvpr2  5442  elunirn  5485  f1veqaeq  5488  isores1  5533  riotauni  5553  riotacl2  5560  riota1  5565  riota1a  5566  snriota  5576  eusvobj2  5577  acexmidlema  5582  acexmidlemb  5583  acexmidlem2  5588  oprabid  5616  0neqopab  5629  brabvv  5630  1stval2  5861  2ndval2  5862  xp1st  5871  xp2nd  5872  unielxp  5879  releldm2  5890  cnvf1o  5925  fo2ndf  5927  poxp  5932  reldmtpos  5950  dftpos4  5960  tpostpos  5961  tpostpos2  5962  iunon  5981  smoel  5997  tfrlem4  6010  tfrlem7  6014  tfrlem8  6015  tfrlem9  6016  nnaord  6198  ecexr  6227  swoord1  6251  swoord2  6252  0er  6256  mapprc  6339  mapsnconst  6381  idssen  6424  ener  6426  en0  6442  en1  6446  en1bg  6447  2dom  6452  enm  6466  xpsnen  6467  ssenen  6497  snnen2og  6505  php5dom  6509  phpm  6511  findcard  6534  findcard2  6535  findcard2s  6536  unfiexmid  6555  eldju2ndl  6670  eldju2ndr  6671  finnum  6714  exmidfodomrlemim  6730  indpi  6804  subhalfnqq  6876  archnqq  6879  enq0sym  6894  nqnq0pi  6900  nqnq0  6903  mulnnnq0  6912  prml  6939  prmu  6940  prssnql  6941  prssnqu  6942  prcdnql  6946  prcunqu  6947  prltlu  6949  prnmaxl  6950  prnminu  6951  prloc  6953  prdisj  6954  addcanprg  7078  recexprlemopl  7087  recexprlemopu  7089  cauappcvgprlemladdfu  7116  caucvgprlemladdfu  7139  recexgt0sr  7222  renfdisj  7449  negf1o  7763  recexre  7955  apsqgt0  7978  apreim  7980  recexaplem2  8019  rerecclap  8095  nn0ge0  8590  elnnnn0b  8609  xnn0xr  8635  xnn0nemnf  8641  xnn0nnn0pnf  8643  znegcl  8677  zeo  8747  nn0ind  8756  nn0ind-raph  8759  uzn0  8929  eluzaddi  8940  eluzsubi  8941  uznn0sub  8945  uz3m2nn  8956  uznnssnn  8960  uz2m1nn  8987  uz2mulcl  8990  indstr2  8991  qmulz  9003  qre  9005  qnegcl  9016  qreccl  9022  rphalflt  9058  nn0ledivnn  9133  xrltnr  9145  nltpnft  9174  ngtmnft  9175  xrrebnd  9176  xnegcl  9189  xnegneg  9190  xltnegi  9192  elioore  9225  elfzuz2  9338  uzsubsubfz  9356  fzdisj  9361  fzmmmeqm  9366  elfz0ubfz0  9427  elfz0fzfz0  9428  fz0fzelfz0  9429  fz0fzdiffz0  9432  elfzmlbp  9434  difelfzle  9436  difelfznle  9437  nn0disj  9439  2ffzeq  9442  fzo1fzo0n0  9483  elfzo0z  9484  elfzo0le  9485  fzonmapblen  9487  fzofzim  9488  elfzodifsumelfzo  9501  elfzonlteqm1  9510  fzonn0p1p1  9513  elfzom1p1elfzo  9514  ssfzo12bi  9525  ubmelm1fzo  9526  fzind2  9539  subfzo0  9542  rebtwn2z  9555  fldiv4p1lem1div2  9601  flqeqceilz  9614  zmodidfzoimp  9650  modfzo0difsn  9691  nnsinds  9738  nn0sinds  9739  expcl2lemap  9804  qexpclz  9813  facp1  9973  facnn2  9977  faclbnd3  9986  bcn1  10001  hashfz0  10068  cvg1nlemres  10245  rexanuz  10248  fclim  10507  climmo  10511  dvdsdivcl  10631  addmodlteqALT  10640  odd2np1  10653  oddge22np1  10661  m1expe  10679  nn0enne  10682  nn0o1gt2  10685  nno  10686  ndvdsadd  10711  infssuzcldc  10727  dfgcd2  10783  mulgcd  10785  ialgfx  10814  prmind2  10882  prm2orodd  10888  prmgt1  10893  oddprmgt2  10895  dfphi2  10976  evenennn  10986  bj-nfalt  11008  decidi  11038  sumdc2  11042  bdel  11079  bdssex  11136  bj-indind  11170  findset  11183  nninfall  11242