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  680  dcim  843  notnotrdc  845  condcOLD  856  pm2.61ddc  863  pm5.18dc  885  pm2.25dc  895  pm2.85dc  907  pm5.12dc  912  pm5.14dc  913  pm5.55dc  915  peircedc  916  pm5.54dc  920  dcand  935  dcor  938  pm5.62dc  948  pm5.63dc  949  pm4.83dc  954  3simpb  998  3simpc  999  3imp  1196  3com12  1210  3com13  1211  syl3anb  1293  xoranor  1397  xorbin  1404  xordc1  1413  biassdc  1415  nfr  1542  nfand  1592  19.21t  1606  19.30dc  1651  exintrbi  1657  19.9t  1666  nfnt  1680  equveli  1783  exdistrfor  1824  sbcof2  1834  sbidm  1875  sbi1v  1916  sbalyz  2028  sbal1yz  2030  nfsb4t  2043  euex  2085  eumo0  2086  mor  2097  exmodc  2105  mo3h  2108  mopick  2133  moexexdc  2139  euexex  2140  2euex  2142  exists2  2152  eqcoms  2209  eleq2s  2301  nfcr  2341  necon3ai  2426  rexnalim  2496  dfrex2dc  2498  rexex  2553  rsp  2554  ralim  2566  rexim  2601  r19.32r  2653  r19.44av  2666  r19.45av  2667  gencl  2805  gencbvex  2820  gencbval  2822  vtoclgf  2832  vtoclg1f  2833  pm13.183  2912  elrabi  2927  eueq2dc  2947  eueq3dc  2948  mob2  2954  euxfr2dc  2959  reu3  2964  rmoim  2975  2rmorex  2980  sbcex  3008  sbcbi2  3050  ra5  3088  sseq1  3217  difdif  3299  dfss4st  3407  difindiss  3428  undif3ss  3435  dfrab3ss  3452  abvor0dc  3485  reldisj  3513  disjel  3516  inssdif0im  3529  uneqdifeqim  3547  r19.2m  3548  r19.2mOLD  3549  r19.3rm  3550  r19.9rmv  3553  rexm  3561  ralm  3565  raaanlem  3566  ifnefalse  3583  ifnotdc  3610  ifandc  3611  ifmdc  3613  nelpri  3658  nelprd  3660  prprc1  3742  difprsn2  3775  diftpsn3  3776  snsssn  3804  preqr2  3812  preq12b  3813  opthpr  3815  prneimg  3817  oprcl  3845  pwprss  3848  intmin4  3915  uniintabim  3924  dfiin2g  3962  iinss2  3982  iundif2ss  3995  disjnim  4037  disjnims  4038  invdisj  4040  disjiun  4042  brne0  4097  brm  4098  trel  4153  trss  4155  ssex  4185  bnd2  4221  abssexg  4230  exmidexmid  4244  rext  4263  unipw  4265  euabex  4273  mss  4274  exss  4275  copsexg  4292  opelopabsb  4310  pwssunim  4335  epelg  4341  sowlin  4371  sotritric  4375  elsuci  4454  sucprc  4463  reusv3  4511  ordon  4538  onsucmin  4559  onsucelsucr  4560  unon  4563  onsucelsucexmid  4582  setind  4591  setind2  4592  sucprcreg  4601  en2lp  4606  eunex  4613  ordsoexmid  4614  ordpwsucss  4619  tfi  4634  peano1  4646  peano2  4647  find  4651  0nelelxp  4708  opelxp  4709  elvvuni  4743  optocl  4755  ralxpf  4828  rexxpf  4829  relop  4832  breldm  4887  dmxpm  4903  elreldm  4909  dmrnssfld  4946  dmcosseq  4955  resabs1  4993  resima2  4998  issref  5070  asymref  5073  xpidtr  5078  trin2  5079  poirr2  5080  xpmlem  5108  dmxpss  5118  xp11m  5126  cnveqb  5143  dfco2a  5188  cores2  5200  coi2  5204  relcnvtr  5207  relresfld  5217  relcnvexb  5227  cnviinm  5229  iotauni  5249  iota1  5251  iota4  5256  iotam  5268  dffun8  5304  fununfun  5322  funcnvsn  5324  imadif  5359  imainlem  5360  fcoi1  5463  fcoi2  5464  f0rn0  5477  f1ocnv  5542  f1ocnvb  5543  fun11iun  5550  ffoss  5561  f1o00  5564  fo00  5565  relelfvdm  5615  nfvres  5617  nfunsn  5618  ssimaex  5647  fvmptss2  5661  fvmptssdm  5671  unpreima  5712  respreima  5715  elrnrexdm  5726  elrnrexdmb  5727  rexrnmpt  5730  dffo4  5735  rnmptss  5748  funiun  5768  funopdmsn  5771  fvpr1  5795  fvpr2  5796  elunirn  5842  f1veqaeq  5845  isores1  5890  iotaexel  5911  riotauni  5913  riotacl2  5920  riota1  5925  riota1a  5926  snriota  5936  eusvobj2  5937  acexmidlema  5942  acexmidlemb  5943  acexmidlem2  5948  oprabid  5983  0neqopab  5997  brabvv  5998  1stval2  6248  2ndval2  6249  xp1st  6258  xp2nd  6259  unielxp  6267  releldm2  6278  cnvf1o  6318  fo2ndf  6320  poxp  6325  reldmtpos  6346  dftpos4  6356  tpostpos  6357  tpostpos2  6358  iunon  6377  smoel  6393  tfrlem4  6406  tfrlem7  6410  tfrlem8  6411  tfrlem9  6412  nnaord  6602  ecexr  6632  swoord1  6656  swoord2  6657  0er  6661  mapprc  6746  mapsnconst  6788  ixpf  6814  mptelixpg  6828  idssen  6875  ener  6878  en0  6894  en1  6898  en1bg  6899  2dom  6904  enm  6922  xpsnen  6923  ssenen  6955  snnen2og  6963  php5dom  6967  phpm  6969  findcard  6992  findcard2  6993  findcard2s  6994  unfiexmid  7022  fiintim  7035  fidcenumlemim  7061  sbthlem1  7066  fiss  7086  djuexb  7153  djuss  7179  eldju2ndl  7181  eldju2ndr  7182  ctssdclemr  7221  exmidlpo  7252  finnum  7297  ficardon  7303  exmidfodomrlemim  7316  acnrcl  7320  3nsssucpw1  7355  indpi  7462  subhalfnqq  7534  archnqq  7537  enq0sym  7552  nqnq0pi  7558  nqnq0  7561  mulnnnq0  7570  prml  7597  prmu  7598  prssnql  7599  prssnqu  7600  prcdnql  7604  prcunqu  7605  prltlu  7607  prnmaxl  7608  prnminu  7609  prloc  7611  prdisj  7612  addcanprg  7736  recexprlemopl  7745  recexprlemopu  7747  cauappcvgprlemladdfu  7774  caucvgprlemladdfu  7797  recexgt0sr  7893  renfdisj  8139  axsuploc  8152  negf1o  8461  recexre  8658  apsqgt0  8681  apreim  8683  aprcl  8726  recexaplem2  8732  rerecclap  8810  nn0ge0  9327  elnnnn0b  9346  xnn0xr  9370  xnn0nemnf  9376  xnn0nnn0pnf  9378  znegcl  9410  zeo  9485  nn0ind  9494  nn0ind-raph  9497  uzn0  9671  eluzaddi  9682  eluzsubi  9683  uznn0sub  9687  uz3m2nn  9701  uznnssnn  9705  uz2m1nn  9733  uz2mulcl  9736  indstr2  9737  qmulz  9751  qre  9753  qnegcl  9764  qreccl  9770  rphalflt  9812  nn0ledivnn  9896  xrltnr  9908  nltpnft  9943  ngtmnft  9946  xrrebnd  9948  xnegcl  9961  xnegneg  9962  xltnegi  9964  xrpnfdc  9971  xrmnfdc  9972  xnegid  9988  xaddid1  9991  xnn0lenn0nn0  9994  xnn0xadd0  9996  xposdif  10011  elioore  10041  elfzuz2  10158  uzsubsubfz  10176  fzdisj  10181  fzmmmeqm  10187  elfz0ubfz0  10254  elfz0fzfz0  10255  fz0fzelfz0  10256  fz0fzdiffz0  10259  elfzmlbp  10261  difelfzle  10263  difelfznle  10264  nn0disj  10267  2ffzeq  10270  fzo1fzo0n0  10314  elfzo0z  10315  elfzo0le  10316  fzonmapblen  10318  fzofzim  10319  elfzodifsumelfzo  10337  elfzonlteqm1  10346  fzonn0p1p1  10349  elfzom1p1elfzo  10350  ssfzo12bi  10361  ubmelm1fzo  10362  fzind2  10375  subfzo0  10378  infssuzcldc  10385  rebtwn2z  10404  fldiv4p1lem1div2  10455  fldiv4lem1div2  10457  flqeqceilz  10470  zmodidfzoimp  10506  modfzo0difsn  10547  nnsinds  10597  nn0sinds  10598  expcl2lemap  10703  qexpclz  10712  zzlesq  10860  facp1  10882  facnn2  10886  faclbnd3  10895  bcn1  10910  hashfz0  10977  wrdf  11007  swrdswrdlem  11163  swrdswrd  11164  cvg1nlemres  11340  rexanuz  11343  fclim  11649  climmo  11653  iser3shft  11701  fsumsplitsn  11765  fsum2dlemstep  11789  fisumcom2  11793  arisum  11853  arisum2  11854  prodmodc  11933  fprodfac  11970  fprod2dlemstep  11977  fprodcom2fi  11981  fprodsplitsn  11988  eftlub  12045  ef01bndlem  12111  sin01gt0  12117  cos01gt0  12118  sin02gt0  12119  dvdsdivcl  12205  addmodlteqALT  12214  odd2np1  12228  oddge22np1  12236  m1expe  12254  nn0enne  12257  nn0o1gt2  12260  nno  12261  ndvdsadd  12286  dfgcd2  12379  mulgcd  12381  algfx  12418  prmind2  12486  prm2orodd  12492  prmgt1  12498  oddprmgt2  12500  dfphi2  12586  nnnn0modprm0  12622  prm23lt5  12630  pythagtriplem2  12633  pcz  12699  dvdsprmpweqnn  12703  oddprmdvds  12721  prmunb  12729  4sqlem4  12759  4sqlem19  12776  evenennn  12808  fngsum  13264  igsumvalx  13265  dfgrp3me  13476  mulgnn0gsum  13508  rngdi  13746  rngdir  13747  dvdsrcl2  13905  unitinvcl  13929  unitinvinv  13930  unitlinv  13932  unitrinv  13933  rmodislmodlem  14156  rmodislmod  14157  zrhval  14423  psrbagf  14476  distop  14601  ntrss  14635  ssntr  14638  lmrcl  14707  lmreltop  14709  txuni2  14772  txcn  14791  hmeocnvb  14834  xmetunirn  14874  blssioo  15069  divcnap  15081  cdivcncfap  15120  dedekindeulemlub  15136  dedekindicclemlub  15145  dvexp2  15228  elply2  15251  plyco  15275  pilem3  15299  sincosq1sgn  15342  sincosq2sgn  15343  sincosq3sgn  15344  sincosq4sgn  15345  sinq12gt0  15346  fsumdvdsmul  15507  zabsle1  15520  lgsdir2lem4  15552  gausslemma2dlem0f  15575  gausslemma2dlem1a  15579  gausslemma2dlem2  15583  gausslemma2dlem3  15584  gausslemma2dlem4  15585  2lgslem1a1  15607  2lgslem3  15622  2lgsoddprmlem3  15632  2lgsoddprm  15634  2sqlem2  15636  2sqlem10  15646  vtxvalprc  15696  iedgvalprc  15697  bj-pm2.18st  15760  bj-dcstab  15766  decidi  15805  sumdc2  15809  bj-charfunbi  15821  bdel  15855  bdssex  15912  bj-indind  15942  findset  15955  nninfall  16020  trirec0  16057  neap0mkv  16082