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  384  mpan10  465  an12s  554  an32s  557  an4s  577  sylnbi  667  dcim  826  notnotrdc  828  const  837  condcOLD  839  pm2.61ddc  846  pm5.18dc  868  pm2.25dc  878  pm2.85dc  890  pm5.12dc  895  pm5.14dc  896  pm5.55dc  898  peircedc  899  pm5.54dc  903  dcor  919  pm5.62dc  929  pm5.63dc  930  pm4.83dc  935  3simpb  979  3simpc  980  3imp  1175  3com12  1185  3com13  1186  syl3anb  1259  xoranor  1355  xorbin  1362  xordc1  1371  biassdc  1373  nfr  1498  nfand  1547  19.21t  1561  19.30dc  1606  exintrbi  1612  19.9t  1621  nfnt  1634  equveli  1732  exdistrfor  1772  sbcof2  1782  sbidm  1823  sbi1v  1863  sbalyz  1972  sbal1yz  1974  nfsb4t  1987  euex  2027  eumo0  2028  mor  2039  exmodc  2047  mo3h  2050  mopick  2075  moexexdc  2081  euexex  2082  2euex  2084  exists2  2094  eqcoms  2140  eleq2s  2232  nfcr  2271  necon3ai  2355  rexnalim  2425  dfrex2dc  2426  rexex  2477  rsp  2478  ralim  2489  rexim  2524  r19.32r  2576  r19.44av  2588  r19.45av  2589  gencl  2713  gencbvex  2727  gencbval  2729  vtoclgf  2739  vtoclg1f  2740  pm13.183  2817  elrabi  2832  eueq2dc  2852  eueq3dc  2853  mob2  2859  euxfr2dc  2864  reu3  2869  rmoim  2880  2rmorex  2885  sbcex  2912  sbcbi2  2954  ra5  2992  sseq1  3115  difdif  3196  dfss4st  3304  difindiss  3325  undif3ss  3332  dfrab3ss  3349  abvor0dc  3381  reldisj  3409  disjel  3412  inssdif0im  3425  uneqdifeqim  3443  r19.2m  3444  r19.2mOLD  3445  r19.3rm  3446  r19.9rmv  3449  rexm  3457  ralm  3462  raaanlem  3463  ifnefalse  3480  ifandc  3503  ifmdc  3504  nelpri  3546  nelprd  3548  prprc1  3626  difprsn2  3655  diftpsn3  3656  snsssn  3683  preqr2  3691  preq12b  3692  opthpr  3694  prneimg  3696  oprcl  3724  pwprss  3727  intmin4  3794  uniintabim  3803  dfiin2g  3841  iinss2  3860  iundif2ss  3873  disjnim  3915  disjnims  3916  invdisj  3918  disjiun  3919  brne0  3972  brm  3973  trel  4028  trss  4030  ssex  4060  bnd2  4092  abssexg  4101  exmidexmid  4115  rext  4132  unipw  4134  euabex  4142  mss  4143  exss  4144  copsexg  4161  opelopabsb  4177  pwssunim  4201  epelg  4207  sowlin  4237  sotritric  4241  elsuci  4320  sucprc  4329  reusv3  4376  ordon  4397  onsucmin  4418  onsucelsucr  4419  unon  4422  onsucelsucexmid  4440  setind  4449  setind2  4450  sucprcreg  4459  en2lp  4464  eunex  4471  ordsoexmid  4472  ordpwsucss  4477  tfi  4491  peano1  4503  peano2  4504  find  4508  0nelelxp  4563  opelxp  4564  elvvuni  4598  optocl  4610  ralxpf  4680  rexxpf  4681  relop  4684  breldm  4738  dmxpm  4754  elreldm  4760  dmrnssfld  4797  dmcosseq  4805  resabs1  4843  resima2  4848  issref  4916  asymref  4919  xpidtr  4924  trin2  4925  poirr2  4926  xpmlem  4954  dmxpss  4964  xp11m  4972  cnveqb  4989  dfco2a  5034  cores2  5046  coi2  5050  relcnvtr  5053  relresfld  5063  relcnvexb  5073  cnviinm  5075  iotauni  5095  iota1  5097  iota4  5101  dffun8  5146  funcnvsn  5163  imadif  5198  imainlem  5199  fcoi1  5298  fcoi2  5299  f0rn0  5312  f1ocnv  5373  f1ocnvb  5374  fun11iun  5381  ffoss  5392  f1o00  5395  fo00  5396  relelfvdm  5446  nfvres  5447  nfunsn  5448  ssimaex  5475  fvmptss2  5489  fvmptssdm  5498  unpreima  5538  respreima  5541  elrnrexdm  5552  elrnrexdmb  5553  rexrnmpt  5556  dffo4  5561  rnmptss  5574  fvpr1  5617  fvpr2  5618  elunirn  5660  f1veqaeq  5663  isores1  5708  riotauni  5729  riotacl2  5736  riota1  5741  riota1a  5742  snriota  5752  eusvobj2  5753  acexmidlema  5758  acexmidlemb  5759  acexmidlem2  5764  oprabid  5796  0neqopab  5809  brabvv  5810  1stval2  6046  2ndval2  6047  xp1st  6056  xp2nd  6057  unielxp  6065  releldm2  6076  cnvf1o  6115  fo2ndf  6117  poxp  6122  reldmtpos  6143  dftpos4  6153  tpostpos  6154  tpostpos2  6155  iunon  6174  smoel  6190  tfrlem4  6203  tfrlem7  6207  tfrlem8  6208  tfrlem9  6209  nnaord  6398  ecexr  6427  swoord1  6451  swoord2  6452  0er  6456  mapprc  6539  mapsnconst  6581  ixpf  6607  mptelixpg  6621  idssen  6664  ener  6666  en0  6682  en1  6686  en1bg  6687  2dom  6692  enm  6707  xpsnen  6708  ssenen  6738  snnen2og  6746  php5dom  6750  phpm  6752  findcard  6775  findcard2  6776  findcard2s  6777  unfiexmid  6799  fiintim  6810  fidcenumlemim  6833  sbthlem1  6838  fiss  6858  djuexb  6922  djuss  6948  eldju2ndl  6950  eldju2ndr  6951  ctssdclemr  6990  exmidlpo  7008  finnum  7032  exmidfodomrlemim  7050  indpi  7143  subhalfnqq  7215  archnqq  7218  enq0sym  7233  nqnq0pi  7239  nqnq0  7242  mulnnnq0  7251  prml  7278  prmu  7279  prssnql  7280  prssnqu  7281  prcdnql  7285  prcunqu  7286  prltlu  7288  prnmaxl  7289  prnminu  7290  prloc  7292  prdisj  7293  addcanprg  7417  recexprlemopl  7426  recexprlemopu  7428  cauappcvgprlemladdfu  7455  caucvgprlemladdfu  7478  recexgt0sr  7574  renfdisj  7817  axsuploc  7830  negf1o  8137  recexre  8333  apsqgt0  8356  apreim  8358  aprcl  8401  recexaplem2  8406  rerecclap  8483  nn0ge0  8995  elnnnn0b  9014  xnn0xr  9038  xnn0nemnf  9044  xnn0nnn0pnf  9046  znegcl  9078  zeo  9149  nn0ind  9158  nn0ind-raph  9161  uzn0  9334  eluzaddi  9345  eluzsubi  9346  uznn0sub  9350  uz3m2nn  9361  uznnssnn  9365  uz2m1nn  9392  uz2mulcl  9395  indstr2  9396  qmulz  9408  qre  9410  qnegcl  9421  qreccl  9427  rphalflt  9464  nn0ledivnn  9547  xrltnr  9559  nltpnft  9590  ngtmnft  9593  xrrebnd  9595  xnegcl  9608  xnegneg  9609  xltnegi  9611  xrpnfdc  9618  xrmnfdc  9619  xnegid  9635  xaddid1  9638  xnn0lenn0nn0  9641  xnn0xadd0  9643  xposdif  9658  elioore  9688  elfzuz2  9802  uzsubsubfz  9820  fzdisj  9825  fzmmmeqm  9831  elfz0ubfz0  9895  elfz0fzfz0  9896  fz0fzelfz0  9897  fz0fzdiffz0  9900  elfzmlbp  9902  difelfzle  9904  difelfznle  9905  nn0disj  9908  2ffzeq  9911  fzo1fzo0n0  9953  elfzo0z  9954  elfzo0le  9955  fzonmapblen  9957  fzofzim  9958  elfzodifsumelfzo  9971  elfzonlteqm1  9980  fzonn0p1p1  9983  elfzom1p1elfzo  9984  ssfzo12bi  9995  ubmelm1fzo  9996  fzind2  10009  subfzo0  10012  rebtwn2z  10025  fldiv4p1lem1div2  10071  flqeqceilz  10084  zmodidfzoimp  10120  modfzo0difsn  10161  nnsinds  10209  nn0sinds  10210  expcl2lemap  10298  qexpclz  10307  facp1  10469  facnn2  10473  faclbnd3  10482  bcn1  10497  hashfz0  10564  cvg1nlemres  10750  rexanuz  10753  fclim  11056  climmo  11060  iser3shft  11108  fsumsplitsn  11172  fsum2dlemstep  11196  fisumcom2  11200  arisum  11260  arisum2  11261  eftlub  11385  ef01bndlem  11452  sin01gt0  11457  cos01gt0  11458  sin02gt0  11459  dvdsdivcl  11537  addmodlteqALT  11546  odd2np1  11559  oddge22np1  11567  m1expe  11585  nn0enne  11588  nn0o1gt2  11591  nno  11592  ndvdsadd  11617  infssuzcldc  11633  dfgcd2  11691  mulgcd  11693  algfx  11722  prmind2  11790  prm2orodd  11796  prmgt1  11801  oddprmgt2  11803  dfphi2  11885  evenennn  11895  distop  12243  ntrss  12277  ssntr  12280  lmrcl  12349  lmreltop  12351  txuni2  12414  txcn  12433  hmeocnvb  12476  xmetunirn  12516  blssioo  12703  divcnap  12713  cdivcncfap  12745  dedekindeulemlub  12756  dedekindicclemlub  12765  dvexp2  12834  pilem3  12853  sincosq1sgn  12896  sincosq2sgn  12897  sincosq3sgn  12898  sincosq4sgn  12899  sinq12gt0  12900  bj-pm2.18st  12947  bj-dcstab  12950  decidi  12991  sumdc2  12995  bdel  13032  bdssex  13089  bj-indind  13119  findset  13132  nninfall  13193