Theorem sylib 122

Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by NM, 3-Jan-1993.)

Hypotheses

Ref	Expression
sylib.1	⊢ (𝜑 → 𝜓)
sylib.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
sylib	⊢ (𝜑 → 𝜒)

Proof of Theorem sylib

Step	Hyp	Ref	Expression
1		sylib.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylib.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3	2	biimpi 120	. 2 ⊢ (𝜓 → 𝜒)
4	1, 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:  sylbb1  137  bicomd  141  pm5.74d  182  bitri  184  3imtr3i  200  ancomd  267  pm4.71d  393  pm4.71rd  394  imdistand  447  orcomd  730  3mix3  1170  mpjao3dan  1318  ecase23d  1361  exlimdh  1610  nexd  1627  alexnim  1662  excomim  1677  19.41  1700  equcomd  1721  nfexd  1775  sbh  1790  sbcof2  1824  sbidm  1865  sb6rf  1867  nfsbt  1995  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  eu2  2089  2euex  2132  eqcomd  2202  3eltr3g  2281  abbid  2313  neneqd  2388  eqnetrrid  2398  3netr3g  2401  necomd  2453  r19.21bi  2585  nrexdv  2590  rexlimd  2611  rabbidva  2751  elisset  2777  euind  2951  rmoan  2964  reuind  2969  2rmorex  2970  spsbc  3001  spesbc  3075  eldifad  3168  eldifbd  3169  3sstr3g  3226  sseqtrdi  3232  difindiss  3418  un00  3498  undifss  3532  ifcldcd  3598  disjpr2  3687  difprsn1  3762  diftpsn3  3764  difsnss  3769  sneqr  3791  preqr1  3799  preq12b  3801  oprcl  3833  intab  3904  riinm  3990  rintm  4010  disjiun  4029  sndisj  4030  3brtr3g  4067  trint  4147  iinexgm  4188  exmidexmid  4230  exmid01  4232  pwntru  4233  exmid1stab  4242  pwel  4252  exss  4261  0nelop  4282  euotd  4288  opelopabsb  4295  pwunim  4322  issod  4355  frind  4388  suctr  4457  orduniss  4461  onelini  4466  oneluni  4467  eusv2i  4491  rexxfrd  4499  rabxfrd  4505  reuhypd  4507  iunpw  4516  sucexg  4535  ordsucim  4537  ordtriexmidlem  4556  ontriexmidim  4559  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  ordsucunielexmid  4568  orddif  4584  suc11g  4594  onintexmid  4610  reg3exmidlemwe  4616  tfisi  4624  peano1  4631  peano2  4632  finds2  4638  omsinds  4659  brrelex12  4702  brel  4716  ssrel  4752  ssrel2  4754  ssrelrel  4764  elrel  4766  xpsspw  4776  relop  4817  dmxpm  4887  opelresi  4958  mptimass  5023  ndmima  5047  poirr2  5063  xpmlem  5091  xpimasn  5119  iotass  5237  iotacl  5244  dffun5r  5271  funeu  5284  funeu2  5285  funfnd  5290  funopg  5293  funun  5303  funinsn  5308  funtp  5312  funcnvuni  5328  funcnvres2  5334  imadiflem  5338  imadif  5339  funimaexglem  5342  fneu2  5366  fnimaeq0  5382  fnmpt  5387  fun2  5434  f00  5452  f0bi  5453  fimadmfo  5492  foimacnv  5525  resdif  5529  f1ococnv1  5536  fv3  5584  relelfvdm  5593  elfvm  5594  nfvres  5595  dffn5im  5609  mptfvex  5650  fvmptdf  5652  fvmptdv2  5654  fndmdif  5670  dff4im  5711  fmpt  5715  fmptd  5719  fmptdf  5722  f1oresrab  5730  fcoconst  5736  fsn  5737  ftpg  5749  fsnunf  5765  resfunexg  5786  isores1  5864  riota2df  5901  acexmidlemcase  5920  brabvv  5972  funoprabg  6025  fnovim  6035  ovmpodf  6058  ovi3  6064  elmpocl  6122  uchoice  6204  1stcof  6230  2ndcof  6231  fnmpo  6269  fmpoco  6283  fo2ndf  6294  f1o2ndf1  6295  disjxp1  6303  brtpos2  6318  reldmtpos  6320  dftpos3  6329  dftpos4  6330  tpostpos2  6332  tposf2  6335  tposf12  6336  tposfo  6338  tposf  6339  smores2  6361  tfrlem1  6375  tfrlem3-2d  6379  tfrlemisucaccv  6392  tfrlemibxssdm  6394  tfrlemibfn  6395  tfrlemi1  6399  tfrexlem  6401  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemaccex  6415  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemaccex  6428  tfrcldm  6430  rdgivallem  6448  rdgisucinc  6452  frecabex  6465  frecfnom  6468  frecfcllem  6471  frecsuclem  6473  omsuc  6539  nntri2  6561  nnsucuniel  6562  nnsseleq  6568  nnm00  6597  ecexr  6606  swoer  6629  elqsn0m  6671  iinerm  6675  erinxp  6677  ecinxp  6678  eroveu  6694  eroprf  6696  mapprc  6720  mapsn  6758  ixpprc  6787  ixp0  6799  resixp  6801  elixpsn  6803  dom2lem  6840  fundmen  6874  dom0  6908  xpf1o  6914  mapxpen  6918  xpmapenlem  6919  ssenen  6921  nneneq  6927  ssfilem  6945  dif1en  6949  dif1enen  6950  fin0  6955  fin0or  6956  diffitest  6957  diffisn  6963  ac6sfi  6968  fimax2gtrilemstep  6970  fimax2gtri  6971  finexdc  6972  exmidpweq  6979  pw1fin  6980  onunsnss  6987  unsnfidcel  6991  undifdcss  6993  undifdc  6994  tpfidceq  7000  fiintim  7001  fisseneq  7004  fidcenumlemr  7030  sbthlemi4  7035  sbthlemi5  7036  sbthlemi9  7040  fifo  7055  suplubti  7075  supelti  7077  infmoti  7103  infisoti  7107  djulclb  7130  updjud  7157  omp1eomlem  7169  0ct  7182  ctmlemr  7183  ctssdclemn0  7185  ctssdccl  7186  ctssdc  7188  enumct  7190  nninfninc  7198  nnnninfeq2  7204  finomni  7215  fodjuomnilemdc  7219  fodjum  7221  fodjuomnilemres  7223  fodjumkvlemres  7234  omniwomnimkv  7242  nninfwlporlem  7248  nninfwlpoimlemginf  7251  nninfwlpoim  7254  nninfinfwlpo  7255  ficardon  7269  exmidonfinlem  7274  en2eleq  7276  exmidfodomrlemeldju  7280  exmidfodomrlemreseldju  7281  exmidfodomrlemim  7282  finacn  7289  acfun  7292  exmidaclem  7293  exmidontriimlem3  7308  exmidontriimlem4  7309  exmidontriim  7310  pw1on  7311  dftap2  7336  2omotaplemst  7343  exmidapne  7345  ccfunen  7349  cc1  7350  cc2lem  7351  cc2  7352  cc3  7353  acnccim  7357  elni2  7400  indpi  7428  distrnqg  7473  subhalfnqq  7500  enq0sym  7518  enq0ref  7519  enq0tr  7520  nqnq0pi  7524  nnnq0lem1  7532  distrnq0  7545  elinp  7560  elnp1st2nd  7562  prltlu  7573  prnmaxl  7574  prnminu  7575  prarloc  7589  nqprm  7628  appdivnq  7649  prmuloc  7652  mullocpr  7657  distrlem4prl  7670  distrlem4pru  7671  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemopu  7689  cauappcvgprlemopl  7732  cauappcvgprlemopu  7734  cauappcvgprlemdisj  7737  cauappcvgprlem2  7746  cauappcvgprlemlim  7747  caucvgprlemnkj  7752  caucvgprlemopl  7755  caucvgprlemopu  7757  caucvgprlemdisj  7760  caucvgprlemcl  7762  caucvgprlemladdfu  7763  caucvgprlemladdrl  7764  caucvgprlem2  7766  caucvgprprlemcbv  7773  caucvgprprlemval  7774  caucvgprprlemlol  7784  caucvgprprlemexbt  7792  caucvgprprlem1  7795  suplocexprlemrl  7803  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemub  7809  suplocexprlemlub  7810  prsrlem1  7828  gt0srpr  7834  caucvgsrlemcl  7875  caucvgsrlembound  7880  caucvgsrlemgt1  7881  suplocsrlemb  7892  suplocsrlem  7894  suplocsr  7895  ltresr  7925  nnindnn  7979  axcaucvglemcl  7981  axcaucvglemval  7983  axcaucvglemcau  7984  axcaucvglemres  7985  axpre-suploclemres  7987  axpre-suploc  7988  sup3exmid  9003  nnind  9025  nn0supp  9320  nn0ge2m1nn  9328  zleloe  9392  zapne  9419  nn0lt2  9426  suprzclex  9443  zindd  9463  uzm1  9651  uzin  9653  infregelbex  9691  elnn1uz2  9700  nn01to3  9710  divfnzn  9714  qapne  9732  xrltnsym2  9888  xaddass  9963  xleadd1a  9967  xlt2add  9974  xlesubadd  9977  iooval2  10009  icoshftf1o  10085  fztri3or  10133  fzneuz  10195  4fvwrd4  10234  elfzo0  10277  infssuzex  10342  infssuzcldc  10344  suprzubdc  10345  nninfdcex  10346  zsupssdc  10347  exbtwnzlemex  10358  ioom  10369  fzfig  10541  uzennn  10547  uzsinds  10555  iseqovex  10569  seq3val  10571  seqvalcd  10572  seqf  10575  seqovcd  10578  monoord2  10597  iseqf1olemjpcl  10619  iseqf1olemqpcl  10620  seq3f1olemqsum  10624  seq3f1o  10628  seqf1og  10632  seq3distr  10643  expp1  10657  expcl2lemap  10662  expclzap  10675  expap0i  10682  nn0ltexp2  10820  bcval5  10874  hashinfuni  10888  hashennnuni  10890  hashnncl  10906  resunimafz0  10942  zfz1isolemiso  10950  zfz1isolem1  10951  zfz1iso  10952  wrdsymb0  10986  wrdlen1  10991  seq3shft  11022  cvg1nlemcau  11168  rexanuz  11172  resqrexlemoverl  11205  resqrexlemglsq  11206  resqrexlemsqa  11208  resqrexlemex  11209  rersqreu  11212  caubnd2  11301  maxleast  11397  fimaxre2  11411  minmax  11414  xrmaxiflemcl  11429  xrmaxiflemab  11431  xrmaxiflemlub  11432  xrmaxadd  11445  xrminmax  11449  xrbdtri  11460  climreu  11481  reccn2ap  11497  iserex  11523  climcvg1nlem  11533  serf0  11536  fz1f1o  11559  summodclem3  11564  zsumdc  11568  fsum3  11571  isumz  11573  isumss  11575  isumss2  11577  fsumsersdc  11579  fsum3ser  11581  fsumsplit  11591  isumclim2  11606  isumclim3  11607  fsum2dlemstep  11618  fsumcnv  11621  fisumcom2  11622  bcxmas  11673  isumle  11679  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  cvgratz  11716  mertenslemub  11718  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  zproddc  11763  prod1dc  11770  fprodsplitdc  11780  fprodsplit  11781  fprodunsn  11788  fprodcl2lem  11789  fprodcllemf  11797  fprod2dlemstep  11806  fprodcnv  11809  fprodcom2fi  11810  fprodle  11824  ef0lem  11844  fsumdvds  12026  mod2eq1n2dvds  12063  ndvdssub  12114  bitsfzolem  12138  bitsfzo  12139  bitsinv1  12146  gcdsupex  12151  gcdsupcl  12152  bezoutlemnewy  12190  bezoutlemmain  12192  bezoutlembi  12199  bezoutlemeu  12201  bezoutlemle  12202  uzwodc  12231  nnwofdc  12232  nnwosdc  12233  nninfctlemfo  12234  nninfct  12235  nn0seqcvgd  12236  eucalgf  12250  eucalginv  12251  lcmval  12258  prmind2  12315  dfphi2  12415  phiprmpw  12417  phimullem  12420  eulerthlem1  12422  eulerthlemrprm  12424  eulerthlema  12425  eulerthlemh  12426  eulerthlemth  12427  eulerth  12428  phisum  12436  odzcllem  12438  odzdvds  12441  pythagtriplem19  12478  pclemub  12483  pcprecl  12485  pceu  12491  pcqmul  12499  pcqcl  12502  pcxnn0cl  12506  pcxqcl  12508  pcge0  12509  pcdvdsb  12516  pceq0  12518  pcneg  12521  pcdvdstr  12523  pcgcd1  12524  pc2dvds  12526  pcz  12528  pcprmpw2  12529  pcaddlem  12535  pcadd  12536  pcmptcl  12538  pcmpt  12539  pcmptdvds  12541  fldivp1  12544  qexpz  12548  pockthlem  12552  pockthg  12553  prmunb  12558  1arith  12563  4sqlemffi  12592  4sqlem17  12603  4sqlem18  12604  4sqlem19  12605  ennnfonelemom  12652  ennnfoneleminc  12655  ennnfonelemhf1o  12657  ennnfonelemex  12658  ennnfonelemhom  12659  ennnfonelemdm  12664  ennnfonelemr  12667  ennnfonelemim  12668  exmidunben  12670  ctinfom  12672  inffinp1  12673  ctinf  12674  enctlem  12676  ctiunctlemu1st  12678  ctiunctlemu2nd  12679  ctiunctlemudc  12681  ctiunct  12684  ctiunctal  12685  unct  12686  ssomct  12689  nninfdclemcl  12692  nninfdclemp1  12694  nninfdc  12697  structcnvcnv  12721  setscom  12745  relelbasov  12767  ressbas2d  12773  ressval3d  12777  ressabsg  12781  restid2  12952  imasaddfnlemg  13018  quslem  13028  ercpbl  13035  fnpr2ob  13044  mgmplusf  13070  grpinvalem  13089  grpinva  13090  grprida  13091  fngsum  13092  igsumvalx  13093  gsum0g  13100  gsumval2  13101  ismnd  13123  mhmpropd  13170  grppropd  13221  grpsubf  13283  dfgrp3mlem  13302  mulgnn0p1  13341  mulgnn0subcl  13343  mulgsubcl  13344  mulgneg  13348  mulgnn0dir  13360  mulgnn0ass  13366  submmulg  13374  issubg2m  13397  issubg4m  13401  ghmmulg  13464  ghmrn  13465  lringuplu  13830  lmodscaf  13944  lssintclm  14018  lspun0  14059  lidlbas  14112  psr1clfi  14318  topontopon  14342  eltg3i  14378  epttop  14412  difopn  14430  uncld  14435  0nnei  14475  resttopon  14493  restabs  14497  restopnb  14503  lmcvg  14539  cnptopco  14544  cnss1  14548  cnss2  14549  cncnpi  14550  cncnp2m  14553  cnrest  14557  cnrest2  14558  cnrest2r  14559  cnptoprest  14561  cnptoprest2  14562  lmss  14568  lmff  14571  lmtopcnp  14572  lmcn  14573  txbasval  14589  upxp  14594  txcnmpt  14595  txdis1cn  14600  txlm  14601  lmcn2  14602  cnmpt11  14605  cnmpt11f  14606  cnmpt1t  14607  cnmpt12  14609  cnmpt21  14613  cnmpt21f  14614  cnmpt2t  14615  cnmpt22  14616  cnmpt22f  14617  cnmptcom  14620  hmeocnv  14629  hmeof1o  14631  hmeores  14637  txhmeo  14641  txswaphmeo  14643  isxmet2d  14670  blfvalps  14707  xblss2ps  14726  xblss2  14727  blfps  14731  blf  14732  unirnblps  14744  unirnbl  14745  isxms2  14774  bdxmet  14823  bdmet  14824  xmetxp  14829  xmettx  14832  blssioo  14875  tgioo  14876  mulcncflem  14929  divcncfap  14936  dedekindeulemuub  14939  dedekindeulemub  14940  dedekindeulemloc  14941  dedekindeulemlu  14943  suplociccreex  14946  suplociccex  14947  dedekindicclemuub  14948  dedekindicclemub  14949  dedekindicclemloc  14950  dedekindicclemlu  14952  dedekindicc  14955  ivthinclemlopn  14958  ivthinclemuopn  14960  ivthdich  14975  limcrcl  14980  limcmpted  14985  limccnp2lem  14998  limccnp2cntop  14999  limccoap  15000  dvrecap  15035  plyaddlem1  15069  plymullem1  15070  plycoeid3  15079  plyco  15081  plycj  15083  plyrecj  15085  dvply1  15087  dvply2g  15088  cosordlem  15171  logbgcd1irraplemexp  15290  logbgcd1irrap  15292  lgsneg1  15352  lgsdilem  15354  lgsdir2  15360  lgsdirprm  15361  lgsdir  15362  lgsne0  15365  lgsabs1  15366  lgsdirnn0  15374  lgsdinn0  15375  gausslemma2dlem1f1o  15387  gausslemma2dlem4  15391  lgseisenlem1  15397  lgsquadlem3  15406  2lgslem1a  15415  2sqlem5  15446  2sqlem7  15448  2sqlem8a  15449  2sqlem8  15450  2sqlem9  15451  bj-stand  15480  bj-charfundcALT  15541  bj-charfunbi  15543  bj-bdfindis  15679  bj-peano4  15687  strcollnfALT  15718  1dom1el  15723  2omap  15728  pwtrufal  15730  pwf1oexmid  15732  subctctexmid  15733  pw1nct  15736  nnsf  15738  nninfalllem1  15741  nninfall  15742  nninfsellemqall  15748  nnnninfen  15754  exmidsbthrlem  15757  sbthom  15761  cvgcmp2nlemabs  15767  trilpo  15778  iswomni0  15786  redcwlpo  15790  dceqnconst  15795  dcapnconst  15796  nconstwlpolem  15800  nconstwlpo  15801  neapmkvlem  15802  neapmkv  15803  ltlenmkv  15805  taupi  15808  alsi1d  15816  alsi2d  15817  alsc1d  15818  alsc2d  15819