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-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbb  122  sylbb2  137  3imtr4i  200  simplbiim  382  mpan10  463  an12s  537  an32s  540  an4s  560  sylnbi  650  dcim  809  notnotrdc  811  const  818  condcOLD  820  pm2.61ddc  827  pm5.18dc  849  pm2.25dc  859  pm2.85dc  871  pm5.12dc  876  pm5.14dc  877  pm5.55dc  879  peircedc  880  pm5.54dc  884  dcor  900  pm5.62dc  910  pm5.63dc  911  pm4.83dc  916  3simpb  960  3simpc  961  3imp  1156  3com12  1166  3com13  1167  syl3anb  1240  xoranor  1336  xorbin  1343  xordc1  1352  biassdc  1354  nfr  1479  nfand  1528  19.21t  1542  19.30dc  1587  exintrbi  1593  19.9t  1602  nfnt  1615  equveli  1713  exdistrfor  1752  sbcof2  1762  sbidm  1803  sbi1v  1843  sbalyz  1948  sbal1yz  1950  nfsb4t  1963  euex  2003  eumo0  2004  mor  2015  exmodc  2023  mo3h  2026  mopick  2051  moexexdc  2057  euexex  2058  2euex  2060  exists2  2070  eqcoms  2116  eleq2s  2207  nfcr  2245  necon3ai  2329  rexnalim  2399  dfrex2dc  2400  rexex  2451  rsp  2452  ralim  2463  rexim  2498  r19.32r  2550  r19.44av  2562  r19.45av  2563  gencl  2687  gencbvex  2701  gencbval  2703  vtoclgf  2713  vtoclg1f  2714  pm13.183  2790  elrabi  2804  eueq2dc  2824  eueq3dc  2825  mob2  2831  euxfr2dc  2836  reu3  2841  rmoim  2852  2rmorex  2857  sbcex  2884  sbcbi2  2925  ra5  2963  sseq1  3084  difdif  3165  dfss4st  3273  difindiss  3294  undif3ss  3301  dfrab3ss  3318  abvor0dc  3350  reldisj  3378  disjel  3381  inssdif0im  3394  uneqdifeqim  3412  r19.2m  3413  r19.2mOLD  3414  r19.3rm  3415  r19.9rmv  3418  rexm  3426  ralm  3431  raaanlem  3432  ifnefalse  3449  ifandc  3472  ifmdc  3473  nelpri  3515  nelprd  3517  prprc1  3595  difprsn2  3624  diftpsn3  3625  snsssn  3652  preqr2  3660  preq12b  3661  opthpr  3663  prneimg  3665  oprcl  3693  pwprss  3696  intmin4  3763  uniintabim  3772  dfiin2g  3810  iinss2  3829  iundif2ss  3842  disjnim  3884  disjnims  3885  invdisj  3887  disjiun  3888  trel  3991  trss  3993  ssex  4023  bnd2  4055  abssexg  4064  exmidexmid  4078  rext  4095  unipw  4097  euabex  4105  mss  4106  exss  4107  copsexg  4124  opelopabsb  4140  pwssunim  4164  epelg  4170  sowlin  4200  sotritric  4204  elsuci  4283  sucprc  4292  reusv3  4339  ordon  4360  onsucmin  4381  onsucelsucr  4382  unon  4385  onsucelsucexmid  4403  setind  4412  setind2  4413  sucprcreg  4422  en2lp  4427  eunex  4434  ordsoexmid  4435  ordpwsucss  4440  tfi  4454  peano1  4466  peano2  4467  find  4471  0nelelxp  4526  opelxp  4527  elvvuni  4561  optocl  4573  ralxpf  4643  rexxpf  4644  relop  4647  breldm  4701  dmxpm  4717  elreldm  4723  dmrnssfld  4758  dmcosseq  4766  resabs1  4804  resima2  4809  issref  4877  asymref  4880  xpidtr  4885  trin2  4886  poirr2  4887  xpmlem  4915  dmxpss  4925  xp11m  4933  cnveqb  4950  dfco2a  4995  cores2  5007  coi2  5011  relcnvtr  5014  relresfld  5024  relcnvexb  5034  cnviinm  5036  iotauni  5056  iota1  5058  iota4  5062  dffun8  5107  funcnvsn  5124  imadif  5159  imainlem  5160  fcoi1  5259  fcoi2  5260  f0rn0  5273  f1ocnv  5334  f1ocnvb  5335  fun11iun  5342  ffoss  5353  f1o00  5356  fo00  5357  relelfvdm  5405  nfvres  5406  nfunsn  5407  ssimaex  5434  fvmptss2  5448  fvmptssdm  5457  unpreima  5497  respreima  5500  elrnrexdm  5511  elrnrexdmb  5512  rexrnmpt  5515  dffo4  5520  rnmptss  5533  fvpr1  5576  fvpr2  5577  elunirn  5619  f1veqaeq  5622  isores1  5667  riotauni  5688  riotacl2  5695  riota1  5700  riota1a  5701  snriota  5711  eusvobj2  5712  acexmidlema  5717  acexmidlemb  5718  acexmidlem2  5723  oprabid  5755  0neqopab  5768  brabvv  5769  1stval2  6004  2ndval2  6005  xp1st  6014  xp2nd  6015  unielxp  6023  releldm2  6034  cnvf1o  6073  fo2ndf  6075  poxp  6080  reldmtpos  6101  dftpos4  6111  tpostpos  6112  tpostpos2  6113  iunon  6132  smoel  6148  tfrlem4  6161  tfrlem7  6165  tfrlem8  6166  tfrlem9  6167  nnaord  6356  ecexr  6385  swoord1  6409  swoord2  6410  0er  6414  mapprc  6497  mapsnconst  6539  ixpf  6565  mptelixpg  6579  idssen  6622  ener  6624  en0  6640  en1  6644  en1bg  6645  2dom  6650  enm  6664  xpsnen  6665  ssenen  6695  snnen2og  6703  php5dom  6707  phpm  6709  findcard  6732  findcard2  6733  findcard2s  6734  unfiexmid  6756  fiintim  6767  fidcenumlemim  6789  sbthlem1  6794  fiss  6814  djuexb  6878  djuss  6904  eldju2ndl  6906  eldju2ndr  6907  ctssdclemr  6946  exmidlpo  6962  finnum  6985  exmidfodomrlemim  7001  indpi  7091  subhalfnqq  7163  archnqq  7166  enq0sym  7181  nqnq0pi  7187  nqnq0  7190  mulnnnq0  7199  prml  7226  prmu  7227  prssnql  7228  prssnqu  7229  prcdnql  7233  prcunqu  7234  prltlu  7236  prnmaxl  7237  prnminu  7238  prloc  7240  prdisj  7241  addcanprg  7365  recexprlemopl  7374  recexprlemopu  7376  cauappcvgprlemladdfu  7403  caucvgprlemladdfu  7426  recexgt0sr  7509  renfdisj  7741  negf1o  8056  recexre  8251  apsqgt0  8274  apreim  8276  recexaplem2  8319  rerecclap  8396  nn0ge0  8899  elnnnn0b  8918  xnn0xr  8942  xnn0nemnf  8948  xnn0nnn0pnf  8950  znegcl  8982  zeo  9053  nn0ind  9062  nn0ind-raph  9065  uzn0  9236  eluzaddi  9247  eluzsubi  9248  uznn0sub  9252  uz3m2nn  9263  uznnssnn  9267  uz2m1nn  9294  uz2mulcl  9297  indstr2  9298  qmulz  9310  qre  9312  qnegcl  9323  qreccl  9329  rphalflt  9365  nn0ledivnn  9440  xrltnr  9452  nltpnft  9483  ngtmnft  9486  xrrebnd  9488  xnegcl  9501  xnegneg  9502  xltnegi  9504  xrpnfdc  9511  xrmnfdc  9512  xnegid  9528  xaddid1  9531  xnn0lenn0nn0  9534  xnn0xadd0  9536  xposdif  9551  elioore  9581  elfzuz2  9695  uzsubsubfz  9713  fzdisj  9718  fzmmmeqm  9724  elfz0ubfz0  9788  elfz0fzfz0  9789  fz0fzelfz0  9790  fz0fzdiffz0  9793  elfzmlbp  9795  difelfzle  9797  difelfznle  9798  nn0disj  9801  2ffzeq  9804  fzo1fzo0n0  9846  elfzo0z  9847  elfzo0le  9848  fzonmapblen  9850  fzofzim  9851  elfzodifsumelfzo  9864  elfzonlteqm1  9873  fzonn0p1p1  9876  elfzom1p1elfzo  9877  ssfzo12bi  9888  ubmelm1fzo  9889  fzind2  9902  subfzo0  9905  rebtwn2z  9918  fldiv4p1lem1div2  9964  flqeqceilz  9977  zmodidfzoimp  10013  modfzo0difsn  10054  nnsinds  10102  nn0sinds  10103  expcl2lemap  10191  qexpclz  10200  facp1  10362  facnn2  10366  faclbnd3  10375  bcn1  10390  hashfz0  10457  cvg1nlemres  10642  rexanuz  10645  fclim  10948  climmo  10952  iser3shft  11000  fsumsplitsn  11064  fsum2dlemstep  11088  fisumcom2  11092  arisum  11152  arisum2  11153  eftlub  11240  ef01bndlem  11307  sin01gt0  11312  cos01gt0  11313  sin02gt0  11314  dvdsdivcl  11389  addmodlteqALT  11398  odd2np1  11411  oddge22np1  11419  m1expe  11437  nn0enne  11440  nn0o1gt2  11443  nno  11444  ndvdsadd  11469  infssuzcldc  11485  dfgcd2  11541  mulgcd  11543  algfx  11572  prmind2  11640  prm2orodd  11646  prmgt1  11651  oddprmgt2  11653  dfphi2  11734  evenennn  11744  distop  12090  ntrss  12124  ssntr  12127  lmrcl  12196  lmreltop  12198  txuni2  12260  txcn  12279  xmetunirn  12340  blssioo  12524  divcnap  12534  cdivcncfap  12566  bj-dcstab  12639  decidi  12681  sumdc2  12685  bdel  12722  bdssex  12779  bj-indind  12809  findset  12822  nninfall  12881