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  532  an32s  535  an4s  555  sylnbi  638  condc  787  notnotrdc  789  pm2.61ddc  796  pm5.18dc  815  dcim  822  pm2.25dc  830  pm2.85dc  849  pm5.12dc  854  pm5.14dc  855  pm5.55dc  857  peircedc  858  pm5.54dc  865  dcor  881  pm5.62dc  891  pm5.63dc  892  pm4.83dc  897  3simpb  941  3simpc  942  3imp  1137  3com12  1147  3com13  1148  syl3anb  1217  xoranor  1313  xorbin  1320  xordc1  1329  biassdc  1331  nfr  1456  nfand  1505  19.21t  1519  19.30dc  1563  exintrbi  1569  19.9t  1578  nfnt  1591  equveli  1689  exdistrfor  1728  sbcof2  1738  sbidm  1779  sbi1v  1819  sbalyz  1923  sbal1yz  1925  nfsb4t  1938  euex  1978  eumo0  1979  mor  1990  exmodc  1998  mo3h  2001  mopick  2026  moexexdc  2032  euexex  2033  2euex  2035  exists2  2045  eqcoms  2091  eleq2s  2182  nfcr  2220  necon3ai  2304  rexnalim  2370  dfrex2dc  2371  rexex  2422  rsp  2423  ralim  2434  rexim  2467  r19.32r  2514  r19.44av  2526  r19.45av  2527  gencl  2651  gencbvex  2665  gencbval  2667  vtoclgf  2677  vtoclg1f  2678  pm13.183  2752  elrabi  2766  eueq2dc  2786  eueq3dc  2787  mob2  2793  euxfr2dc  2798  reu3  2803  rmoim  2814  2rmorex  2819  sbcex  2846  sbcbi2  2887  ra5  2925  sseq1  3045  difdif  3123  dfss4st  3230  difindiss  3251  undif3ss  3258  dfrab3ss  3275  abvor0dc  3304  reldisj  3331  disjel  3334  inssdif0im  3347  uneqdifeqim  3364  r19.2m  3365  r19.3rm  3366  r19.9rmv  3369  rexm  3377  ralm  3382  raaanlem  3383  ifnefalse  3400  ifandc  3423  ifmdc  3424  nelpri  3465  nelprd  3467  prprc1  3545  difprsn2  3572  diftpsn3  3573  snsssn  3600  preqr2  3608  preq12b  3609  opthpr  3611  prneimg  3613  oprcl  3641  pwprss  3644  intmin4  3711  uniintabim  3720  dfiin2g  3758  iinss2  3777  iundif2ss  3790  disjnim  3828  disjnims  3829  invdisj  3831  disjiun  3832  trel  3935  trss  3937  ssex  3968  bnd2  4000  abssexg  4008  exmidexmid  4022  rext  4033  unipw  4035  euabex  4043  mss  4044  exss  4045  copsexg  4062  opelopabsb  4078  pwssunim  4102  epelg  4108  sowlin  4138  sotritric  4142  elsuci  4221  sucprc  4230  reusv3  4273  ordon  4293  onsucmin  4314  onsucelsucr  4315  unon  4318  onsucelsucexmid  4336  setind  4345  setind2  4346  sucprcreg  4355  en2lp  4360  eunex  4367  ordsoexmid  4368  ordpwsucss  4373  tfi  4387  peano1  4399  peano2  4400  find  4404  0nelelxp  4456  opelxp  4457  elvvuni  4490  optocl  4502  ralxpf  4570  rexxpf  4571  relop  4574  breldm  4628  dmxpm  4644  elreldm  4649  dmrnssfld  4684  dmcosseq  4692  resabs1  4729  resima2  4733  issref  4801  asymref  4804  xpidtr  4809  trin2  4810  poirr2  4811  xpmlem  4839  dmxpss  4848  xp11m  4856  cnveqb  4873  dfco2a  4918  cores2  4930  coi2  4934  relcnvtr  4937  relresfld  4947  relcnvexb  4957  cnviinm  4959  iotauni  4979  iota1  4981  iota4  4985  dffun8  5029  funcnvsn  5045  imadif  5080  imainlem  5081  fcoi1  5175  fcoi2  5176  f0rn0  5189  f1ocnv  5250  f1ocnvb  5251  fun11iun  5258  ffoss  5269  f1o00  5272  fo00  5273  relelfvdm  5320  nfvres  5321  nfunsn  5322  ssimaex  5349  fvmptss2  5363  fvmptssdm  5371  unpreima  5408  respreima  5411  elrnrexdm  5422  elrnrexdmb  5423  rexrnmpt  5426  dffo4  5431  rnmptss  5443  fvpr1  5483  fvpr2  5484  elunirn  5527  f1veqaeq  5530  isores1  5575  riotauni  5596  riotacl2  5603  riota1  5608  riota1a  5609  snriota  5619  eusvobj2  5620  acexmidlema  5625  acexmidlemb  5626  acexmidlem2  5631  oprabid  5663  0neqopab  5676  brabvv  5677  1stval2  5908  2ndval2  5909  xp1st  5918  xp2nd  5919  unielxp  5926  releldm2  5937  cnvf1o  5972  fo2ndf  5974  poxp  5979  reldmtpos  6000  dftpos4  6010  tpostpos  6011  tpostpos2  6012  iunon  6031  smoel  6047  tfrlem4  6060  tfrlem7  6064  tfrlem8  6065  tfrlem9  6066  nnaord  6248  ecexr  6277  swoord1  6301  swoord2  6302  0er  6306  mapprc  6389  mapsnconst  6431  idssen  6474  ener  6476  en0  6492  en1  6496  en1bg  6497  2dom  6502  enm  6516  xpsnen  6517  ssenen  6547  snnen2og  6555  php5dom  6559  phpm  6561  findcard  6584  findcard2  6585  findcard2s  6586  unfiexmid  6608  fidcenumlemim  6640  sbthlem1  6645  eldju2ndl  6742  eldju2ndr  6743  finnum  6790  exmidfodomrlemim  6806  indpi  6880  subhalfnqq  6952  archnqq  6955  enq0sym  6970  nqnq0pi  6976  nqnq0  6979  mulnnnq0  6988  prml  7015  prmu  7016  prssnql  7017  prssnqu  7018  prcdnql  7022  prcunqu  7023  prltlu  7025  prnmaxl  7026  prnminu  7027  prloc  7029  prdisj  7030  addcanprg  7154  recexprlemopl  7163  recexprlemopu  7165  cauappcvgprlemladdfu  7192  caucvgprlemladdfu  7215  recexgt0sr  7298  renfdisj  7525  negf1o  7839  recexre  8031  apsqgt0  8054  apreim  8056  recexaplem2  8095  rerecclap  8171  nn0ge0  8668  elnnnn0b  8687  xnn0xr  8711  xnn0nemnf  8717  xnn0nnn0pnf  8719  znegcl  8751  zeo  8821  nn0ind  8830  nn0ind-raph  8833  uzn0  9003  eluzaddi  9014  eluzsubi  9015  uznn0sub  9019  uz3m2nn  9030  uznnssnn  9034  uz2m1nn  9061  uz2mulcl  9064  indstr2  9065  qmulz  9077  qre  9079  qnegcl  9090  qreccl  9096  rphalflt  9132  nn0ledivnn  9207  xrltnr  9219  nltpnft  9248  ngtmnft  9249  xrrebnd  9250  xnegcl  9263  xnegneg  9264  xltnegi  9266  elioore  9299  elfzuz2  9412  uzsubsubfz  9430  fzdisj  9435  fzmmmeqm  9440  elfz0ubfz0  9501  elfz0fzfz0  9502  fz0fzelfz0  9503  fz0fzdiffz0  9506  elfzmlbp  9508  difelfzle  9510  difelfznle  9511  nn0disj  9514  2ffzeq  9517  fzo1fzo0n0  9559  elfzo0z  9560  elfzo0le  9561  fzonmapblen  9563  fzofzim  9564  elfzodifsumelfzo  9577  elfzonlteqm1  9586  fzonn0p1p1  9589  elfzom1p1elfzo  9590  ssfzo12bi  9601  ubmelm1fzo  9602  fzind2  9615  subfzo0  9618  rebtwn2z  9631  fldiv4p1lem1div2  9677  flqeqceilz  9690  zmodidfzoimp  9726  modfzo0difsn  9767  nnsinds  9814  nn0sinds  9815  expcl2lemap  9932  qexpclz  9941  facp1  10103  facnn2  10107  faclbnd3  10116  bcn1  10131  hashfz0  10198  cvg1nlemres  10383  rexanuz  10386  fclim  10646  climmo  10650  iser3shft  10699  fsumsplitsn  10767  fsum2dlemstep  10791  fisumcom2  10795  arisum  10853  arisum2  10854  dvdsdivcl  10944  addmodlteqALT  10953  odd2np1  10966  oddge22np1  10974  m1expe  10992  nn0enne  10995  nn0o1gt2  10998  nno  10999  ndvdsadd  11024  infssuzcldc  11040  dfgcd2  11096  mulgcd  11098  ialgfx  11127  prmind2  11195  prm2orodd  11201  prmgt1  11206  oddprmgt2  11208  dfphi2  11289  evenennn  11299  bj-nfalt  11322  decidi  11352  sumdc2  11356  bdel  11393  bdssex  11450  bj-indind  11484  findset  11497  nninfall  11557