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  734  3mix3  1192  mpjao3dan  1341  ecase23d  1384  exlimdh  1642  nexd  1659  alexnim  1694  excomim  1709  19.41  1732  equcomd  1753  nfexd  1807  sbh  1822  sbcof2  1856  sbidm  1897  sb6rf  1899  nfsbt  2027  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  eu2  2122  2euex  2165  eqcomd  2235  3eltr3g  2314  abbid  2346  neneqd  2421  eqnetrrid  2431  3netr3g  2434  necomd  2486  r19.21bi  2618  nrexdv  2623  rexlimd  2645  rabbidva  2788  elisset  2815  euind  2991  rmoan  3004  reuind  3009  2rmorex  3010  spsbc  3041  spesbc  3116  eldifad  3209  eldifbd  3210  3sstr3g  3267  sseqtrdi  3273  difindiss  3459  un00  3539  undifss  3573  ifcldcd  3641  disjpr2  3731  difprsn1  3810  diftpsn3  3812  difsnss  3817  sneqr  3841  preqr1  3849  preq12b  3851  oprcl  3884  intab  3955  riinm  4041  rintm  4061  disjiun  4081  sndisj  4082  3brtr3g  4119  trint  4200  iinexgm  4242  exmidexmid  4284  exmid01  4286  pwntru  4287  exmid1stab  4296  pwel  4308  exss  4317  0nelop  4338  euotd  4345  opelopabsb  4352  pwunim  4381  issod  4414  frind  4447  suctr  4516  orduniss  4520  onelini  4525  oneluni  4526  eusv2i  4550  rexxfrd  4558  rabxfrd  4564  reuhypd  4566  iunpw  4575  sucexg  4594  ordsucim  4596  ordtriexmidlem  4615  ontriexmidim  4618  ordtri2or2exmidlem  4622  onsucelsucexmidlem  4625  ordsucunielexmid  4627  orddif  4643  suc11g  4653  onintexmid  4669  reg3exmidlemwe  4675  tfisi  4683  peano1  4690  peano2  4691  finds2  4697  omsinds  4718  brrelex12  4762  brel  4776  ssrel  4812  ssrel2  4814  ssrelrel  4824  elrel  4826  xpsspw  4836  relop  4878  dmxpm  4950  opelresi  5022  mptimass  5087  ndmima  5111  poirr2  5127  xpmlem  5155  xpimasn  5183  iotass  5302  iotacl  5309  dffun5r  5336  funeu  5349  funeu2  5350  funfnd  5355  funopg  5358  funun  5368  fununfun  5370  funinsn  5376  funtp  5380  funcnvuni  5396  funcnvres2  5402  imadiflem  5406  imadif  5407  funimaexglem  5410  fneu2  5434  fnimaeq0  5451  fnmpt  5456  fun2  5506  f00  5525  f0bi  5526  fimadmfo  5565  foimacnv  5598  resdif  5602  f1ococnv1  5609  fv3  5658  relelfvdm  5667  elfvm  5668  nfvres  5671  dffn5im  5687  mptfvex  5728  fvmptdf  5730  fvmptdv2  5732  fndmdif  5748  dff4im  5789  fmpt  5793  fmptd  5797  fmptdf  5800  f1oresrab  5808  fcoconst  5814  fsn  5815  funopsn  5825  ftpg  5833  fsnunf  5849  resfunexg  5870  isores1  5950  riota2df  5988  acexmidlemcase  6008  brabvv  6062  funoprabg  6115  fnovim  6125  ovmpodf  6148  ovi3  6154  elmpocl  6212  uchoice  6295  1stcof  6321  2ndcof  6322  opabn1stprc  6353  fnmpo  6362  fmpoco  6376  fo2ndf  6387  f1o2ndf1  6388  disjxp1  6396  brtpos2  6412  reldmtpos  6414  dftpos3  6423  dftpos4  6424  tpostpos2  6426  tposf2  6429  tposf12  6430  tposfo  6432  tposf  6433  smores2  6455  tfrlem1  6469  tfrlem3-2d  6473  tfrlemisucaccv  6486  tfrlemibxssdm  6488  tfrlemibfn  6489  tfrlemi1  6493  tfrexlem  6495  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemaccex  6509  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemaccex  6522  tfrcldm  6524  rdgivallem  6542  rdgisucinc  6546  frecabex  6559  frecfnom  6562  frecfcllem  6565  frecsuclem  6567  omsuc  6635  nntri2  6657  nnsucuniel  6658  nnsseleq  6664  nnm00  6693  ecexr  6702  swoer  6725  elqsn0m  6767  iinerm  6771  erinxp  6773  ecinxp  6774  eroveu  6790  eroprf  6792  mapprc  6816  mapsn  6854  ixpprc  6883  ixp0  6895  resixp  6897  elixpsn  6899  dom2lem  6940  fundmen  6976  1dom1el  6988  dom0  7019  xpf1o  7025  mapxpen  7029  xpmapenlem  7030  ssenen  7032  nneneq  7038  ssfilem  7057  ssfilemd  7059  dif1en  7063  dif1enen  7064  fin0  7069  fin0or  7070  diffitest  7071  diffisn  7077  ac6sfi  7082  fimax2gtrilemstep  7085  fimax2gtri  7086  finexdc  7087  eqsndc  7090  exmidpweq  7096  pw1fin  7097  onunsnss  7104  unsnfidcel  7108  undifdcss  7110  undifdc  7111  tpfidceq  7117  fiintim  7118  fisseneq  7121  fidcenumlemr  7148  sbthlemi4  7153  sbthlemi5  7154  sbthlemi9  7158  fifo  7173  suplubti  7193  supelti  7195  infmoti  7221  infisoti  7225  djulclb  7248  updjud  7275  omp1eomlem  7287  0ct  7300  ctmlemr  7301  ctssdclemn0  7303  ctssdccl  7304  ctssdc  7306  enumct  7308  nninfninc  7316  nnnninfeq2  7322  finomni  7333  fodjuomnilemdc  7337  fodjum  7339  fodjuomnilemres  7341  fodjumkvlemres  7352  omniwomnimkv  7360  nninfwlporlem  7366  nninfwlpoimlemginf  7369  nninfwlpoim  7372  nninfinfwlpo  7373  ficardon  7387  pr2cv1  7394  exmidonfinlem  7397  en2eleq  7399  exmidfodomrlemeldju  7403  exmidfodomrlemreseldju  7404  exmidfodomrlemim  7405  finacn  7412  acfun  7415  exmidaclem  7416  exmidontriimlem3  7431  exmidontriimlem4  7432  exmidontriim  7433  pw1if  7436  pw1on  7437  dftap2  7463  2omotaplemst  7470  exmidapne  7472  ccfunen  7476  cc1  7477  cc2lem  7478  cc2  7479  cc3  7480  acnccim  7484  elni2  7527  indpi  7555  distrnqg  7600  subhalfnqq  7627  enq0sym  7645  enq0ref  7646  enq0tr  7647  nqnq0pi  7651  nnnq0lem1  7659  distrnq0  7672  elinp  7687  elnp1st2nd  7689  prltlu  7700  prnmaxl  7701  prnminu  7702  prarloc  7716  nqprm  7755  appdivnq  7776  prmuloc  7779  mullocpr  7784  distrlem4prl  7797  distrlem4pru  7798  ltexprlemm  7813  ltexprlemopl  7814  ltexprlemopu  7816  cauappcvgprlemopl  7859  cauappcvgprlemopu  7861  cauappcvgprlemdisj  7864  cauappcvgprlem2  7873  cauappcvgprlemlim  7874  caucvgprlemnkj  7879  caucvgprlemopl  7882  caucvgprlemopu  7884  caucvgprlemdisj  7887  caucvgprlemcl  7889  caucvgprlemladdfu  7890  caucvgprlemladdrl  7891  caucvgprlem2  7893  caucvgprprlemcbv  7900  caucvgprprlemval  7901  caucvgprprlemlol  7911  caucvgprprlemexbt  7919  caucvgprprlem1  7922  suplocexprlemrl  7930  suplocexprlemmu  7931  suplocexprlemru  7932  suplocexprlemdisj  7933  suplocexprlemloc  7934  suplocexprlemub  7936  suplocexprlemlub  7937  prsrlem1  7955  gt0srpr  7961  caucvgsrlemcl  8002  caucvgsrlembound  8007  caucvgsrlemgt1  8008  suplocsrlemb  8019  suplocsrlem  8021  suplocsr  8022  ltresr  8052  nnindnn  8106  axcaucvglemcl  8108  axcaucvglemval  8110  axcaucvglemcau  8111  axcaucvglemres  8112  axpre-suploclemres  8114  axpre-suploc  8115  sup3exmid  9130  nnind  9152  nn0supp  9447  nn0ge2m1nn  9455  zleloe  9519  zapne  9547  nn0lt2  9554  suprzclex  9571  zindd  9591  uzm1  9780  uzin  9782  infregelbex  9825  elnn1uz2  9834  nn01to3  9844  divfnzn  9848  qapne  9866  xrltnsym2  10022  xaddass  10097  xleadd1a  10101  xlt2add  10108  xlesubadd  10111  iooval2  10143  icoshftf1o  10219  fztri3or  10267  fzneuz  10329  4fvwrd4  10368  elfzo0  10414  infssuzex  10486  infssuzcldc  10488  suprzubdc  10489  nninfdcex  10490  zsupssdc  10491  exbtwnzlemex  10502  ioom  10513  fzfig  10685  uzennn  10691  uzsinds  10699  iseqovex  10713  seq3val  10715  seqvalcd  10716  seqf  10719  seqovcd  10722  monoord2  10741  iseqf1olemjpcl  10763  iseqf1olemqpcl  10764  seq3f1olemqsum  10768  seq3f1o  10772  seqf1og  10776  seq3distr  10787  expp1  10801  expcl2lemap  10806  expclzap  10819  expap0i  10826  nn0ltexp2  10964  bcval5  11018  hashinfuni  11032  hashennnuni  11034  hashnncl  11050  resunimafz0  11088  zfz1isolemiso  11096  zfz1isolem1  11097  zfz1iso  11098  wrdsymb0  11139  wrdlen1  11144  ccat1st1st  11211  swrdrlen  11235  pfxid  11260  pfxwrdsymbg  11264  pfxtrcfv  11267  pfxccat1  11276  pfxpfxid  11283  pfxcctswrd  11284  swrdccatin1  11299  pfxccatin12  11307  pfxccatid  11315  seq3shft  11392  cvg1nlemcau  11538  rexanuz  11542  resqrexlemoverl  11575  resqrexlemglsq  11576  resqrexlemsqa  11578  resqrexlemex  11579  rersqreu  11582  caubnd2  11671  maxleast  11767  fimaxre2  11781  minmax  11784  xrmaxiflemcl  11799  xrmaxiflemab  11801  xrmaxiflemlub  11802  xrmaxadd  11815  xrminmax  11819  xrbdtri  11830  climreu  11851  reccn2ap  11867  iserex  11893  climcvg1nlem  11903  serf0  11906  fz1f1o  11929  summodclem3  11934  zsumdc  11938  fsum3  11941  isumz  11943  isumss  11945  isumss2  11947  fsumsersdc  11949  fsum3ser  11951  fsumsplit  11961  isumclim2  11976  isumclim3  11977  fsum2dlemstep  11988  fsumcnv  11991  fisumcom2  11992  bcxmas  12043  isumle  12049  cvgratnnlemnexp  12078  cvgratnnlemmn  12079  cvgratz  12086  mertenslemub  12088  mertenslemi1  12089  mertenslem2  12090  mertensabs  12091  zproddc  12133  prod1dc  12140  fprodsplitdc  12150  fprodsplit  12151  fprodunsn  12158  fprodcl2lem  12159  fprodcllemf  12167  fprod2dlemstep  12176  fprodcnv  12179  fprodcom2fi  12180  fprodle  12194  ef0lem  12214  fsumdvds  12396  mod2eq1n2dvds  12433  ndvdssub  12484  bitsfzolem  12508  bitsfzo  12509  bitsinv1  12516  gcdsupex  12521  gcdsupcl  12522  bezoutlemnewy  12560  bezoutlemmain  12562  bezoutlembi  12569  bezoutlemeu  12571  bezoutlemle  12572  uzwodc  12601  nnwofdc  12602  nnwosdc  12603  nninfctlemfo  12604  nninfct  12605  nn0seqcvgd  12606  eucalgf  12620  eucalginv  12621  lcmval  12628  prmind2  12685  dfphi2  12785  phiprmpw  12787  phimullem  12790  eulerthlem1  12792  eulerthlemrprm  12794  eulerthlema  12795  eulerthlemh  12796  eulerthlemth  12797  eulerth  12798  phisum  12806  odzcllem  12808  odzdvds  12811  pythagtriplem19  12848  pclemub  12853  pcprecl  12855  pceu  12861  pcqmul  12869  pcqcl  12872  pcxnn0cl  12876  pcxqcl  12878  pcge0  12879  pcdvdsb  12886  pceq0  12888  pcneg  12891  pcdvdstr  12893  pcgcd1  12894  pc2dvds  12896  pcz  12898  pcprmpw2  12899  pcaddlem  12905  pcadd  12906  pcmptcl  12908  pcmpt  12909  pcmptdvds  12911  fldivp1  12914  qexpz  12918  pockthlem  12922  pockthg  12923  prmunb  12928  1arith  12933  4sqlemffi  12962  4sqlem17  12973  4sqlem18  12974  4sqlem19  12975  ennnfonelemom  13022  ennnfoneleminc  13025  ennnfonelemhf1o  13027  ennnfonelemex  13028  ennnfonelemhom  13029  ennnfonelemdm  13034  ennnfonelemr  13037  ennnfonelemim  13038  exmidunben  13040  ctinfom  13042  inffinp1  13043  ctinf  13044  enctlem  13046  ctiunctlemu1st  13048  ctiunctlemu2nd  13049  ctiunctlemudc  13051  ctiunct  13054  ctiunctal  13055  unct  13056  ssomct  13059  nninfdclemcl  13062  nninfdclemp1  13064  nninfdc  13067  structcnvcnv  13091  setscom  13115  relelbasov  13138  ressbas2d  13144  ressval3d  13148  ressabsg  13152  restid2  13324  imasaddfnlemg  13390  quslem  13400  ercpbl  13407  fnpr2ob  13416  mgmplusf  13442  grpinvalem  13461  grpinva  13462  grprida  13463  fngsum  13464  igsumvalx  13465  gsum0g  13472  gsumval2  13473  ismnd  13495  mhmpropd  13542  grppropd  13593  grpsubf  13655  dfgrp3mlem  13674  mulgnn0p1  13713  mulgnn0subcl  13715  mulgsubcl  13716  mulgneg  13720  mulgnn0dir  13732  mulgnn0ass  13738  submmulg  13746  issubg2m  13769  issubg4m  13773  ghmmulg  13836  ghmrn  13837  lringuplu  14203  lmodscaf  14317  lssintclm  14391  lspun0  14432  lidlbas  14485  psr1clfi  14695  topontopon  14737  eltg3i  14773  epttop  14807  difopn  14825  uncld  14830  0nnei  14870  resttopon  14888  restabs  14892  restopnb  14898  lmcvg  14934  cnptopco  14939  cnss1  14943  cnss2  14944  cncnpi  14945  cncnp2m  14948  cnrest  14952  cnrest2  14953  cnrest2r  14954  cnptoprest  14956  cnptoprest2  14957  lmss  14963  lmff  14966  lmtopcnp  14967  lmcn  14968  txbasval  14984  upxp  14989  txcnmpt  14990  txdis1cn  14995  txlm  14996  lmcn2  14997  cnmpt11  15000  cnmpt11f  15001  cnmpt1t  15002  cnmpt12  15004  cnmpt21  15008  cnmpt21f  15009  cnmpt2t  15010  cnmpt22  15011  cnmpt22f  15012  cnmptcom  15015  hmeocnv  15024  hmeof1o  15026  hmeores  15032  txhmeo  15036  txswaphmeo  15038  isxmet2d  15065  blfvalps  15102  xblss2ps  15121  xblss2  15122  blfps  15126  blf  15127  unirnblps  15139  unirnbl  15140  isxms2  15169  bdxmet  15218  bdmet  15219  xmetxp  15224  xmettx  15227  blssioo  15270  tgioo  15271  mulcncflem  15324  divcncfap  15331  dedekindeulemuub  15334  dedekindeulemub  15335  dedekindeulemloc  15336  dedekindeulemlu  15338  suplociccreex  15341  suplociccex  15342  dedekindicclemuub  15343  dedekindicclemub  15344  dedekindicclemloc  15345  dedekindicclemlu  15347  dedekindicc  15350  ivthinclemlopn  15353  ivthinclemuopn  15355  ivthdich  15370  limcrcl  15375  limcmpted  15380  limccnp2lem  15393  limccnp2cntop  15394  limccoap  15395  dvrecap  15430  plyaddlem1  15464  plymullem1  15465  plycoeid3  15474  plyco  15476  plycj  15478  plyrecj  15480  dvply1  15482  dvply2g  15483  cosordlem  15566  logbgcd1irraplemexp  15685  logbgcd1irrap  15687  lgsneg1  15747  lgsdilem  15749  lgsdir2  15755  lgsdirprm  15756  lgsdir  15757  lgsne0  15760  lgsabs1  15761  lgsdirnn0  15769  lgsdinn0  15770  gausslemma2dlem1f1o  15782  gausslemma2dlem4  15786  lgseisenlem1  15792  lgsquadlem3  15801  2lgslem1a  15810  2sqlem5  15841  2sqlem7  15843  2sqlem8a  15844  2sqlem8  15845  2sqlem9  15846  gropeld  15893  grstructeld2dom  15894  uhgrm  15922  upgrm  15944  upgr1een  15968  uhgredgm  15980  edgupgren  15985  edgumgren  15986  edgusgren  16007  ausgrusgrben  16012  umgr2edg1  16053  usgredg2vlem1  16066  uhgr0enedgfi  16080  vtxedgfi  16100  vtxlpfi  16101  vtxdumgrfival  16109  vtxd0nedgbfi  16110  1hevtxdg0fi  16118  p1evtxdeqfilem  16122  wlkvtxm  16151  g0wlk0  16181  wlkres  16188  trlreslem  16198  clwwlkccatlem  16209  clwwlknnn  16221  bj-stand  16294  bj-charfundcALT  16354  bj-charfunbi  16356  bj-bdfindis  16492  bj-peano4  16500  strcollnfALT  16531  2omap  16544  pw1map  16546  pwtrufal  16548  pwf1oexmid  16550  subctctexmid  16551  pw1nct  16554  nnsf  16557  nninfalllem1  16560  nninfall  16561  nninfsellemqall  16567  nnnninfen  16573  exmidsbthrlem  16576  sbthom  16580  cvgcmp2nlemabs  16586  trilpo  16597  iswomni0  16605  redcwlpo  16609  dceqnconst  16614  dcapnconst  16615  nconstwlpolem  16619  nconstwlpo  16620  neapmkvlem  16621  neapmkv  16622  ltlenmkv  16624  taupi  16627  gfsumval  16630  gsumgfsum  16634  alsi1d  16642  alsi2d  16643  alsc1d  16644  alsc2d  16645