Theorem sylbi 121

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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylbb  123  sylbb2  138  3imtr4i  201  simplbiim  387  mpan10  474  an12s  565  an32s  568  an4s  588  sylnbi  679  dcim  842  notnotrdc  844  condcOLD  855  pm2.61ddc  862  pm5.18dc  884  pm2.25dc  894  pm2.85dc  906  pm5.12dc  911  pm5.14dc  912  pm5.55dc  914  peircedc  915  pm5.54dc  919  dcand  934  dcor  937  pm5.62dc  947  pm5.63dc  948  pm4.83dc  953  3simpb  997  3simpc  998  3imp  1195  3com12  1209  3com13  1210  syl3anb  1292  xoranor  1388  xorbin  1395  xordc1  1404  biassdc  1406  nfr  1532  nfand  1582  19.21t  1596  19.30dc  1641  exintrbi  1647  19.9t  1656  nfnt  1670  equveli  1773  exdistrfor  1814  sbcof2  1824  sbidm  1865  sbi1v  1906  sbalyz  2018  sbal1yz  2020  nfsb4t  2033  euex  2075  eumo0  2076  mor  2087  exmodc  2095  mo3h  2098  mopick  2123  moexexdc  2129  euexex  2130  2euex  2132  exists2  2142  eqcoms  2199  eleq2s  2291  nfcr  2331  necon3ai  2416  rexnalim  2486  dfrex2dc  2488  rexex  2543  rsp  2544  ralim  2556  rexim  2591  r19.32r  2643  r19.44av  2656  r19.45av  2657  gencl  2795  gencbvex  2810  gencbval  2812  vtoclgf  2822  vtoclg1f  2823  pm13.183  2902  elrabi  2917  eueq2dc  2937  eueq3dc  2938  mob2  2944  euxfr2dc  2949  reu3  2954  rmoim  2965  2rmorex  2970  sbcex  2998  sbcbi2  3040  ra5  3078  sseq1  3207  difdif  3289  dfss4st  3397  difindiss  3418  undif3ss  3425  dfrab3ss  3442  abvor0dc  3475  reldisj  3503  disjel  3506  inssdif0im  3519  uneqdifeqim  3537  r19.2m  3538  r19.2mOLD  3539  r19.3rm  3540  r19.9rmv  3543  rexm  3551  ralm  3555  raaanlem  3556  ifnefalse  3573  ifnotdc  3599  ifandc  3600  ifmdc  3602  nelpri  3647  nelprd  3649  prprc1  3731  difprsn2  3763  diftpsn3  3764  snsssn  3792  preqr2  3800  preq12b  3801  opthpr  3803  prneimg  3805  oprcl  3833  pwprss  3836  intmin4  3903  uniintabim  3912  dfiin2g  3950  iinss2  3970  iundif2ss  3983  disjnim  4025  disjnims  4026  invdisj  4028  disjiun  4029  brne0  4083  brm  4084  trel  4139  trss  4141  ssex  4171  bnd2  4207  abssexg  4216  exmidexmid  4230  rext  4249  unipw  4251  euabex  4259  mss  4260  exss  4261  copsexg  4278  opelopabsb  4295  pwssunim  4320  epelg  4326  sowlin  4356  sotritric  4360  elsuci  4439  sucprc  4448  reusv3  4496  ordon  4523  onsucmin  4544  onsucelsucr  4545  unon  4548  onsucelsucexmid  4567  setind  4576  setind2  4577  sucprcreg  4586  en2lp  4591  eunex  4598  ordsoexmid  4599  ordpwsucss  4604  tfi  4619  peano1  4631  peano2  4632  find  4636  0nelelxp  4693  opelxp  4694  elvvuni  4728  optocl  4740  ralxpf  4813  rexxpf  4814  relop  4817  breldm  4871  dmxpm  4887  elreldm  4893  dmrnssfld  4930  dmcosseq  4938  resabs1  4976  resima2  4981  issref  5053  asymref  5056  xpidtr  5061  trin2  5062  poirr2  5063  xpmlem  5091  dmxpss  5101  xp11m  5109  cnveqb  5126  dfco2a  5171  cores2  5183  coi2  5187  relcnvtr  5190  relresfld  5200  relcnvexb  5210  cnviinm  5212  iotauni  5232  iota1  5234  iota4  5239  iotam  5251  dffun8  5287  funcnvsn  5304  imadif  5339  imainlem  5340  fcoi1  5441  fcoi2  5442  f0rn0  5455  f1ocnv  5520  f1ocnvb  5521  fun11iun  5528  ffoss  5539  f1o00  5542  fo00  5543  relelfvdm  5593  nfvres  5595  nfunsn  5596  ssimaex  5625  fvmptss2  5639  fvmptssdm  5649  unpreima  5690  respreima  5693  elrnrexdm  5704  elrnrexdmb  5705  rexrnmpt  5708  dffo4  5713  rnmptss  5726  fvpr1  5769  fvpr2  5770  elunirn  5816  f1veqaeq  5819  isores1  5864  iotaexel  5885  riotauni  5887  riotacl2  5894  riota1  5899  riota1a  5900  snriota  5910  eusvobj2  5911  acexmidlema  5916  acexmidlemb  5917  acexmidlem2  5922  oprabid  5957  0neqopab  5971  brabvv  5972  1stval2  6222  2ndval2  6223  xp1st  6232  xp2nd  6233  unielxp  6241  releldm2  6252  cnvf1o  6292  fo2ndf  6294  poxp  6299  reldmtpos  6320  dftpos4  6330  tpostpos  6331  tpostpos2  6332  iunon  6351  smoel  6367  tfrlem4  6380  tfrlem7  6384  tfrlem8  6385  tfrlem9  6386  nnaord  6576  ecexr  6606  swoord1  6630  swoord2  6631  0er  6635  mapprc  6720  mapsnconst  6762  ixpf  6788  mptelixpg  6802  idssen  6845  ener  6847  en0  6863  en1  6867  en1bg  6868  2dom  6873  enm  6888  xpsnen  6889  ssenen  6921  snnen2og  6929  php5dom  6933  phpm  6935  findcard  6958  findcard2  6959  findcard2s  6960  unfiexmid  6988  fiintim  7001  fidcenumlemim  7027  sbthlem1  7032  fiss  7052  djuexb  7119  djuss  7145  eldju2ndl  7147  eldju2ndr  7148  ctssdclemr  7187  exmidlpo  7218  finnum  7263  ficardon  7269  exmidfodomrlemim  7282  acnrcl  7286  3nsssucpw1  7321  indpi  7428  subhalfnqq  7500  archnqq  7503  enq0sym  7518  nqnq0pi  7524  nqnq0  7527  mulnnnq0  7536  prml  7563  prmu  7564  prssnql  7565  prssnqu  7566  prcdnql  7570  prcunqu  7571  prltlu  7573  prnmaxl  7574  prnminu  7575  prloc  7577  prdisj  7578  addcanprg  7702  recexprlemopl  7711  recexprlemopu  7713  cauappcvgprlemladdfu  7740  caucvgprlemladdfu  7763  recexgt0sr  7859  renfdisj  8105  axsuploc  8118  negf1o  8427  recexre  8624  apsqgt0  8647  apreim  8649  aprcl  8692  recexaplem2  8698  rerecclap  8776  nn0ge0  9293  elnnnn0b  9312  xnn0xr  9336  xnn0nemnf  9342  xnn0nnn0pnf  9344  znegcl  9376  zeo  9450  nn0ind  9459  nn0ind-raph  9462  uzn0  9636  eluzaddi  9647  eluzsubi  9648  uznn0sub  9652  uz3m2nn  9666  uznnssnn  9670  uz2m1nn  9698  uz2mulcl  9701  indstr2  9702  qmulz  9716  qre  9718  qnegcl  9729  qreccl  9735  rphalflt  9777  nn0ledivnn  9861  xrltnr  9873  nltpnft  9908  ngtmnft  9911  xrrebnd  9913  xnegcl  9926  xnegneg  9927  xltnegi  9929  xrpnfdc  9936  xrmnfdc  9937  xnegid  9953  xaddid1  9956  xnn0lenn0nn0  9959  xnn0xadd0  9961  xposdif  9976  elioore  10006  elfzuz2  10123  uzsubsubfz  10141  fzdisj  10146  fzmmmeqm  10152  elfz0ubfz0  10219  elfz0fzfz0  10220  fz0fzelfz0  10221  fz0fzdiffz0  10224  elfzmlbp  10226  difelfzle  10228  difelfznle  10229  nn0disj  10232  2ffzeq  10235  fzo1fzo0n0  10278  elfzo0z  10279  elfzo0le  10280  fzonmapblen  10282  fzofzim  10283  elfzodifsumelfzo  10296  elfzonlteqm1  10305  fzonn0p1p1  10308  elfzom1p1elfzo  10309  ssfzo12bi  10320  ubmelm1fzo  10321  fzind2  10334  subfzo0  10337  infssuzcldc  10344  rebtwn2z  10363  fldiv4p1lem1div2  10414  fldiv4lem1div2  10416  flqeqceilz  10429  zmodidfzoimp  10465  modfzo0difsn  10506  nnsinds  10556  nn0sinds  10557  expcl2lemap  10662  qexpclz  10671  zzlesq  10819  facp1  10841  facnn2  10845  faclbnd3  10854  bcn1  10869  hashfz0  10936  wrdf  10960  cvg1nlemres  11169  rexanuz  11172  fclim  11478  climmo  11482  iser3shft  11530  fsumsplitsn  11594  fsum2dlemstep  11618  fisumcom2  11622  arisum  11682  arisum2  11683  prodmodc  11762  fprodfac  11799  fprod2dlemstep  11806  fprodcom2fi  11810  fprodsplitsn  11817  eftlub  11874  ef01bndlem  11940  sin01gt0  11946  cos01gt0  11947  sin02gt0  11948  dvdsdivcl  12034  addmodlteqALT  12043  odd2np1  12057  oddge22np1  12065  m1expe  12083  nn0enne  12086  nn0o1gt2  12089  nno  12090  ndvdsadd  12115  dfgcd2  12208  mulgcd  12210  algfx  12247  prmind2  12315  prm2orodd  12321  prmgt1  12327  oddprmgt2  12329  dfphi2  12415  nnnn0modprm0  12451  prm23lt5  12459  pythagtriplem2  12462  pcz  12528  dvdsprmpweqnn  12532  oddprmdvds  12550  prmunb  12558  4sqlem4  12588  4sqlem19  12605  evenennn  12637  fngsum  13092  igsumvalx  13093  dfgrp3me  13304  mulgnn0gsum  13336  rngdi  13574  rngdir  13575  dvdsrcl2  13733  unitinvcl  13757  unitinvinv  13758  unitlinv  13760  unitrinv  13761  rmodislmodlem  13984  rmodislmod  13985  zrhval  14251  psrbagf  14302  distop  14407  ntrss  14441  ssntr  14444  lmrcl  14513  lmreltop  14515  txuni2  14578  txcn  14597  hmeocnvb  14640  xmetunirn  14680  blssioo  14875  divcnap  14887  cdivcncfap  14926  dedekindeulemlub  14942  dedekindicclemlub  14951  dvexp2  15034  elply2  15057  plyco  15081  pilem3  15105  sincosq1sgn  15148  sincosq2sgn  15149  sincosq3sgn  15150  sincosq4sgn  15151  sinq12gt0  15152  fsumdvdsmul  15313  zabsle1  15326  lgsdir2lem4  15358  gausslemma2dlem0f  15381  gausslemma2dlem1a  15385  gausslemma2dlem2  15389  gausslemma2dlem3  15390  gausslemma2dlem4  15391  2lgslem1a1  15413  2lgslem3  15428  2lgsoddprmlem3  15438  2lgsoddprm  15440  2sqlem2  15442  2sqlem10  15452  bj-pm2.18st  15482  bj-dcstab  15488  decidi  15527  sumdc2  15531  bj-charfunbi  15543  bdel  15577  bdssex  15634  bj-indind  15664  findset  15677  nninfall  15742  trirec0  15779  neap0mkv  15804