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  567  an32s  570  an4s  592  sylnbi  684  dcim  848  notnotrdc  850  condcOLD  861  pm2.61ddc  868  pm5.18dc  890  pm2.25dc  900  pm2.85dc  912  pm5.12dc  917  pm5.14dc  918  pm5.55dc  920  peircedc  921  pm5.54dc  925  dcand  940  dcor  943  pm5.62dc  953  pm5.63dc  954  pm4.83dc  959  ifp2  988  ifpor  995  1fpid3  1002  3simpb  1021  3simpc  1022  3imp  1219  3com12  1233  3com13  1234  syl3anb  1316  xoranor  1421  xorbin  1428  xordc1  1437  biassdc  1439  nfr  1566  nfand  1616  19.21t  1630  19.30dc  1675  exintrbi  1681  19.9t  1690  nfnt  1704  equveli  1807  exdistrfor  1848  sbcof2  1858  sbidm  1899  sbi1v  1940  sbalyz  2052  sbal1yz  2054  nfsb4t  2067  euex  2109  eumo0  2110  mor  2122  exmodc  2130  mo3h  2133  mopick  2158  moexexdc  2164  euexex  2165  2euex  2167  exists2  2177  eqcoms  2234  eleq2s  2326  nfcr  2366  necon3ai  2451  rexnalim  2521  dfrex2dc  2523  rexex  2578  rsp  2579  ralim  2591  rexim  2626  r19.32r  2679  r19.44av  2692  r19.45av  2693  gencl  2835  gencbvex  2850  gencbval  2852  vtoclgf  2862  vtoclg1f  2863  pm13.183  2944  elrabi  2959  eueq2dc  2979  eueq3dc  2980  mob2  2986  euxfr2dc  2991  reu3  2996  rmoim  3007  2rmorex  3012  sbcex  3040  sbcbi2  3082  ra5  3121  sseq1  3250  difdif  3332  dfss4st  3440  difindiss  3461  undif3ss  3468  dfrab3ss  3485  abvor0dc  3518  reldisj  3546  disjel  3549  inssdif0im  3562  uneqdifeqim  3580  r19.2m  3581  r19.2mOLD  3582  r19.3rm  3583  r19.9rmv  3586  rexm  3594  ralm  3598  raaanlem  3599  ifnefalse  3616  ifnotdc  3644  ifandc  3646  ifmdc  3648  nelpri  3693  nelprd  3695  prprc1  3780  difprsn2  3813  diftpsn3  3814  snsssn  3844  preqr2  3852  preq12b  3853  opthpr  3855  prneimg  3857  oprcl  3886  pwprss  3889  intmin4  3956  uniintabim  3965  dfiin2g  4003  iinss2  4023  iundif2ss  4036  disjnim  4078  disjnims  4079  invdisj  4081  disjiun  4083  brne0  4138  brm  4139  trel  4194  trss  4196  ssex  4226  bnd2  4263  abssexg  4272  exmidexmid  4286  rext  4307  unipw  4309  euabex  4317  mss  4318  exss  4319  copsexg  4336  opelopabsb  4354  pwssunim  4381  epelg  4387  sowlin  4417  sotritric  4421  elsuci  4500  sucprc  4509  reusv3  4557  ordon  4584  onsucmin  4605  onsucelsucr  4606  unon  4609  onsucelsucexmid  4628  setind  4637  setind2  4638  sucprcreg  4647  en2lp  4652  eunex  4659  ordsoexmid  4660  ordpwsucss  4665  tfi  4680  peano1  4692  peano2  4693  find  4697  0nelelxp  4754  opelxp  4755  elvvuni  4790  optocl  4802  ralxpf  4876  rexxpf  4877  relop  4880  breldm  4935  reldmm  4950  dmxpm  4952  elreldm  4958  dmrnssfld  4995  dmcosseq  5004  resabs1  5042  resima2  5047  issref  5119  asymref  5122  xpidtr  5127  trin2  5128  poirr2  5129  xpmlem  5157  dmxpss  5167  xp11m  5175  cnveqb  5192  dfco2a  5237  cores2  5249  coi2  5253  relcnvtr  5256  relresfld  5266  relcnvexb  5276  cnviinm  5278  iotauni  5299  iota1  5301  iota4  5306  iotam  5318  dffun8  5354  fununfun  5373  funcnvsn  5375  imadif  5410  imainlem  5411  fcoi1  5517  fcoi2  5518  f0rn0  5531  f1ocnv  5596  f1ocnvb  5597  fun11iun  5604  ffoss  5616  f1o00  5620  fo00  5621  relelfvdm  5671  nfvres  5675  nfunsn  5676  ssimaex  5707  fvmptss2  5721  fvmptssdm  5731  unpreima  5772  respreima  5775  elrnrexdm  5786  elrnrexdmb  5787  rexrnmpt  5790  dffo4  5795  rnmptss  5808  funiun  5829  funopdmsn  5834  fvpr1  5858  fvpr2  5859  elunirn  5907  f1veqaeq  5910  isores1  5955  iotaexel  5976  riotauni  5978  riotacl2  5986  riota1  5991  riota1a  5992  snriota  6003  eusvobj2  6004  acexmidlema  6009  acexmidlemb  6010  acexmidlem2  6015  oprabid  6050  0neqopab  6066  brabvv  6067  1stval2  6318  2ndval2  6319  xp1st  6328  xp2nd  6329  unielxp  6337  releldm2  6348  cnvf1o  6390  fo2ndf  6392  poxp  6397  reldmtpos  6419  dftpos4  6429  tpostpos  6430  tpostpos2  6431  iunon  6450  smoel  6466  tfrlem4  6479  tfrlem7  6483  tfrlem8  6484  tfrlem9  6485  nnaord  6677  ecexr  6707  swoord1  6731  swoord2  6732  0er  6736  mapprc  6821  mapsnconst  6863  ixpf  6889  mptelixpg  6903  idssen  6950  ener  6953  en0  6969  en1  6973  en1bg  6974  2dom  6980  modom  6994  enm  7004  xpsnen  7005  ssenen  7037  snnen2og  7045  php5dom  7049  phpm  7052  findcard  7077  findcard2  7078  findcard2s  7079  unfiexmid  7110  fiintim  7123  fidcenumlemim  7151  sbthlem1  7156  fiss  7176  djuexb  7243  djuss  7269  eldju2ndl  7271  eldju2ndr  7272  ctssdclemr  7311  exmidlpo  7342  finnum  7387  ficardon  7393  exmidfodomrlemim  7412  acnrcl  7416  3nsssucpw1  7454  indpi  7562  subhalfnqq  7634  archnqq  7637  enq0sym  7652  nqnq0pi  7658  nqnq0  7661  mulnnnq0  7670  prml  7697  prmu  7698  prssnql  7699  prssnqu  7700  prcdnql  7704  prcunqu  7705  prltlu  7707  prnmaxl  7708  prnminu  7709  prloc  7711  prdisj  7712  addcanprg  7836  recexprlemopl  7845  recexprlemopu  7847  cauappcvgprlemladdfu  7874  caucvgprlemladdfu  7897  recexgt0sr  7993  renfdisj  8239  axsuploc  8252  negf1o  8561  recexre  8758  apsqgt0  8781  apreim  8783  aprcl  8826  recexaplem2  8832  rerecclap  8910  nn0ge0  9427  elnnnn0b  9446  xnn0xr  9470  xnn0nemnf  9476  xnn0nnn0pnf  9478  znegcl  9510  zeo  9585  nn0ind  9594  nn0ind-raph  9597  uzn0  9772  eluzaddi  9783  eluzsubi  9784  uznn0sub  9788  uz3m2nn  9807  uznnssnn  9811  uz2m1nn  9839  uz2mulcl  9842  indstr2  9843  qmulz  9857  qre  9859  qnegcl  9870  qreccl  9876  rphalflt  9918  nn0ledivnn  10002  xrltnr  10014  nltpnft  10049  ngtmnft  10052  xrrebnd  10054  xnegcl  10067  xnegneg  10068  xltnegi  10070  xrpnfdc  10077  xrmnfdc  10078  xnegid  10094  xaddid1  10097  xnn0lenn0nn0  10100  xnn0xadd0  10102  xposdif  10117  elioore  10147  elfzuz2  10264  uzsubsubfz  10282  fzdisj  10287  fzmmmeqm  10293  elfz0ubfz0  10360  elfz0fzfz0  10361  fz0fzelfz0  10362  fz0fzdiffz0  10365  elfzmlbp  10367  difelfzle  10369  difelfznle  10370  nn0disj  10373  2ffzeq  10376  fzo1fzo0n0  10423  elfzo0z  10424  elfzo0le  10425  fzonmapblen  10427  fzofzim  10428  elfzodifsumelfzo  10447  elfzonlteqm1  10456  fzonn0p1p1  10459  elfzom1p1elfzo  10460  ssfzo12bi  10471  ubmelm1fzo  10472  fzind2  10486  subfzo0  10489  infssuzcldc  10496  rebtwn2z  10515  fldiv4p1lem1div2  10566  fldiv4lem1div2  10568  flqeqceilz  10581  zmodidfzoimp  10617  modfzo0difsn  10658  nnsinds  10708  nn0sinds  10709  expcl2lemap  10814  qexpclz  10823  zzlesq  10971  facp1  10993  facnn2  10997  faclbnd3  11006  bcn1  11021  hashfz0  11090  wrdf  11120  swrdswrdlem  11286  swrdswrd  11287  swrdccatin1  11307  pfxccatin12lem2a  11309  pfxccatin12lem1  11310  swrdccatin2  11311  pfxccatin12lem2  11313  pfxccatin12lem3  11314  pfxccatin12  11315  pfxccat3  11316  swrdccat  11317  swrdccat3blem  11321  cvg1nlemres  11547  rexanuz  11550  fclim  11856  climmo  11860  iser3shft  11908  fsumsplitsn  11973  fsum2dlemstep  11997  fisumcom2  12001  arisum  12061  arisum2  12062  prodmodc  12141  fprodfac  12178  fprod2dlemstep  12185  fprodcom2fi  12189  fprodsplitsn  12196  eftlub  12253  ef01bndlem  12319  sin01gt0  12325  cos01gt0  12326  sin02gt0  12327  dvdsdivcl  12413  addmodlteqALT  12422  odd2np1  12436  oddge22np1  12444  m1expe  12462  nn0enne  12465  nn0o1gt2  12468  nno  12469  ndvdsadd  12494  dfgcd2  12587  mulgcd  12589  algfx  12626  prmind2  12694  prm2orodd  12700  prmgt1  12706  oddprmgt2  12708  dfphi2  12794  nnnn0modprm0  12830  prm23lt5  12838  pythagtriplem2  12841  pcz  12907  dvdsprmpweqnn  12911  oddprmdvds  12929  prmunb  12937  4sqlem4  12967  4sqlem19  12984  evenennn  13016  fngsum  13473  igsumvalx  13474  dfgrp3me  13685  mulgnn0gsum  13717  rngdi  13956  rngdir  13957  dvdsrcl2  14116  unitinvcl  14140  unitinvinv  14141  unitlinv  14143  unitrinv  14144  rmodislmodlem  14367  rmodislmod  14368  zrhval  14634  psrbagf  14687  distop  14812  ntrss  14846  ssntr  14849  lmrcl  14919  txuni2  14983  txcn  15002  hmeocnvb  15045  xmetunirn  15085  blssioo  15280  divcnap  15292  cdivcncfap  15331  dedekindeulemlub  15347  dedekindicclemlub  15356  dvexp2  15439  elply2  15462  plyco  15486  pilem3  15510  sincosq1sgn  15553  sincosq2sgn  15554  sincosq3sgn  15555  sincosq4sgn  15556  sinq12gt0  15557  fsumdvdsmul  15718  zabsle1  15731  lgsdir2lem4  15763  gausslemma2dlem0f  15786  gausslemma2dlem1a  15790  gausslemma2dlem2  15794  gausslemma2dlem3  15795  gausslemma2dlem4  15796  2lgslem1a1  15818  2lgslem3  15833  2lgsoddprmlem3  15843  2lgsoddprm  15845  2sqlem2  15847  2sqlem10  15857  vtxvalprc  15909  iedgvalprc  15910  upgrex  15957  umgredg  15999  ausgrusgrben  16022  usgruspgrben  16040  usgrislfuspgrdom  16044  uhgr2edg  16060  uspgredg2v  16075  griedg0ssusgr  16105  subusgr  16129  wlkv  16180  wlk1walkdom  16213  trlsv  16238  trlf1  16242  clwwlk1loop  16253  clwwlkext2edg  16276  umgr2cwwkdifex  16279  clwwlknonex2lem2  16292  clwwlknonex2e  16294  eupthv  16300  eupth2lem3lem4fi  16327  bj-pm2.18st  16367  bj-dcstab  16373  decidi  16412  sumdc2  16416  bj-charfunbi  16427  bdel  16461  bdssex  16518  bj-indind  16548  findset  16561  nninfall  16632  trirec0  16669  neap0mkv  16694