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  2787  elisset  2814  euind  2990  rmoan  3003  reuind  3008  2rmorex  3009  spsbc  3040  spesbc  3115  eldifad  3208  eldifbd  3209  3sstr3g  3266  sseqtrdi  3272  difindiss  3458  un00  3538  undifss  3572  ifcldcd  3640  disjpr2  3730  difprsn1  3807  diftpsn3  3809  difsnss  3814  sneqr  3838  preqr1  3846  preq12b  3848  oprcl  3881  intab  3952  riinm  4038  rintm  4058  disjiun  4078  sndisj  4079  3brtr3g  4116  trint  4197  iinexgm  4239  exmidexmid  4281  exmid01  4283  pwntru  4284  exmid1stab  4293  pwel  4305  exss  4314  0nelop  4335  euotd  4342  opelopabsb  4349  pwunim  4378  issod  4411  frind  4444  suctr  4513  orduniss  4517  onelini  4522  oneluni  4523  eusv2i  4547  rexxfrd  4555  rabxfrd  4561  reuhypd  4563  iunpw  4572  sucexg  4591  ordsucim  4593  ordtriexmidlem  4612  ontriexmidim  4615  ordtri2or2exmidlem  4619  onsucelsucexmidlem  4622  ordsucunielexmid  4624  orddif  4640  suc11g  4650  onintexmid  4666  reg3exmidlemwe  4672  tfisi  4680  peano1  4687  peano2  4688  finds2  4694  omsinds  4715  brrelex12  4759  brel  4773  ssrel  4809  ssrel2  4811  ssrelrel  4821  elrel  4823  xpsspw  4833  relop  4875  dmxpm  4947  opelresi  5019  mptimass  5084  ndmima  5108  poirr2  5124  xpmlem  5152  xpimasn  5180  iotass  5299  iotacl  5306  dffun5r  5333  funeu  5346  funeu2  5347  funfnd  5352  funopg  5355  funun  5365  fununfun  5367  funinsn  5373  funtp  5377  funcnvuni  5393  funcnvres2  5399  imadiflem  5403  imadif  5404  funimaexglem  5407  fneu2  5431  fnimaeq0  5448  fnmpt  5453  fun2  5503  f00  5522  f0bi  5523  fimadmfo  5562  foimacnv  5595  resdif  5599  f1ococnv1  5606  fv3  5655  relelfvdm  5664  elfvm  5665  nfvres  5668  dffn5im  5684  mptfvex  5725  fvmptdf  5727  fvmptdv2  5729  fndmdif  5745  dff4im  5786  fmpt  5790  fmptd  5794  fmptdf  5797  f1oresrab  5805  fcoconst  5811  fsn  5812  funopsn  5822  ftpg  5830  fsnunf  5846  resfunexg  5867  isores1  5947  riota2df  5985  acexmidlemcase  6005  brabvv  6059  funoprabg  6112  fnovim  6122  ovmpodf  6145  ovi3  6151  elmpocl  6209  uchoice  6292  1stcof  6318  2ndcof  6319  opabn1stprc  6350  fnmpo  6359  fmpoco  6373  fo2ndf  6384  f1o2ndf1  6385  disjxp1  6393  brtpos2  6408  reldmtpos  6410  dftpos3  6419  dftpos4  6420  tpostpos2  6422  tposf2  6425  tposf12  6426  tposfo  6428  tposf  6429  smores2  6451  tfrlem1  6465  tfrlem3-2d  6469  tfrlemisucaccv  6482  tfrlemibxssdm  6484  tfrlemibfn  6485  tfrlemi1  6489  tfrexlem  6491  tfr1onlemsucaccv  6498  tfr1onlembxssdm  6500  tfr1onlembfn  6501  tfr1onlemaccex  6505  tfrcllemsucaccv  6511  tfrcllembxssdm  6513  tfrcllembfn  6514  tfrcllemaccex  6518  tfrcldm  6520  rdgivallem  6538  rdgisucinc  6542  frecabex  6555  frecfnom  6558  frecfcllem  6561  frecsuclem  6563  omsuc  6631  nntri2  6653  nnsucuniel  6654  nnsseleq  6660  nnm00  6689  ecexr  6698  swoer  6721  elqsn0m  6763  iinerm  6767  erinxp  6769  ecinxp  6770  eroveu  6786  eroprf  6788  mapprc  6812  mapsn  6850  ixpprc  6879  ixp0  6891  resixp  6893  elixpsn  6895  dom2lem  6936  fundmen  6972  dom0  7012  xpf1o  7018  mapxpen  7022  xpmapenlem  7023  ssenen  7025  nneneq  7031  ssfilem  7050  dif1en  7054  dif1enen  7055  fin0  7060  fin0or  7061  diffitest  7062  diffisn  7068  ac6sfi  7073  fimax2gtrilemstep  7076  fimax2gtri  7077  finexdc  7078  eqsndc  7081  exmidpweq  7087  pw1fin  7088  onunsnss  7095  unsnfidcel  7099  undifdcss  7101  undifdc  7102  tpfidceq  7108  fiintim  7109  fisseneq  7112  fidcenumlemr  7138  sbthlemi4  7143  sbthlemi5  7144  sbthlemi9  7148  fifo  7163  suplubti  7183  supelti  7185  infmoti  7211  infisoti  7215  djulclb  7238  updjud  7265  omp1eomlem  7277  0ct  7290  ctmlemr  7291  ctssdclemn0  7293  ctssdccl  7294  ctssdc  7296  enumct  7298  nninfninc  7306  nnnninfeq2  7312  finomni  7323  fodjuomnilemdc  7327  fodjum  7329  fodjuomnilemres  7331  fodjumkvlemres  7342  omniwomnimkv  7350  nninfwlporlem  7356  nninfwlpoimlemginf  7359  nninfwlpoim  7362  nninfinfwlpo  7363  ficardon  7377  pr2cv1  7384  exmidonfinlem  7387  en2eleq  7389  exmidfodomrlemeldju  7393  exmidfodomrlemreseldju  7394  exmidfodomrlemim  7395  finacn  7402  acfun  7405  exmidaclem  7406  exmidontriimlem3  7421  exmidontriimlem4  7422  exmidontriim  7423  pw1if  7426  pw1on  7427  dftap2  7453  2omotaplemst  7460  exmidapne  7462  ccfunen  7466  cc1  7467  cc2lem  7468  cc2  7469  cc3  7470  acnccim  7474  elni2  7517  indpi  7545  distrnqg  7590  subhalfnqq  7617  enq0sym  7635  enq0ref  7636  enq0tr  7637  nqnq0pi  7641  nnnq0lem1  7649  distrnq0  7662  elinp  7677  elnp1st2nd  7679  prltlu  7690  prnmaxl  7691  prnminu  7692  prarloc  7706  nqprm  7745  appdivnq  7766  prmuloc  7769  mullocpr  7774  distrlem4prl  7787  distrlem4pru  7788  ltexprlemm  7803  ltexprlemopl  7804  ltexprlemopu  7806  cauappcvgprlemopl  7849  cauappcvgprlemopu  7851  cauappcvgprlemdisj  7854  cauappcvgprlem2  7863  cauappcvgprlemlim  7864  caucvgprlemnkj  7869  caucvgprlemopl  7872  caucvgprlemopu  7874  caucvgprlemdisj  7877  caucvgprlemcl  7879  caucvgprlemladdfu  7880  caucvgprlemladdrl  7881  caucvgprlem2  7883  caucvgprprlemcbv  7890  caucvgprprlemval  7891  caucvgprprlemlol  7901  caucvgprprlemexbt  7909  caucvgprprlem1  7912  suplocexprlemrl  7920  suplocexprlemmu  7921  suplocexprlemru  7922  suplocexprlemdisj  7923  suplocexprlemloc  7924  suplocexprlemub  7926  suplocexprlemlub  7927  prsrlem1  7945  gt0srpr  7951  caucvgsrlemcl  7992  caucvgsrlembound  7997  caucvgsrlemgt1  7998  suplocsrlemb  8009  suplocsrlem  8011  suplocsr  8012  ltresr  8042  nnindnn  8096  axcaucvglemcl  8098  axcaucvglemval  8100  axcaucvglemcau  8101  axcaucvglemres  8102  axpre-suploclemres  8104  axpre-suploc  8105  sup3exmid  9120  nnind  9142  nn0supp  9437  nn0ge2m1nn  9445  zleloe  9509  zapne  9537  nn0lt2  9544  suprzclex  9561  zindd  9581  uzm1  9770  uzin  9772  infregelbex  9810  elnn1uz2  9819  nn01to3  9829  divfnzn  9833  qapne  9851  xrltnsym2  10007  xaddass  10082  xleadd1a  10086  xlt2add  10093  xlesubadd  10096  iooval2  10128  icoshftf1o  10204  fztri3or  10252  fzneuz  10314  4fvwrd4  10353  elfzo0  10399  infssuzex  10470  infssuzcldc  10472  suprzubdc  10473  nninfdcex  10474  zsupssdc  10475  exbtwnzlemex  10486  ioom  10497  fzfig  10669  uzennn  10675  uzsinds  10683  iseqovex  10697  seq3val  10699  seqvalcd  10700  seqf  10703  seqovcd  10706  monoord2  10725  iseqf1olemjpcl  10747  iseqf1olemqpcl  10748  seq3f1olemqsum  10752  seq3f1o  10756  seqf1og  10760  seq3distr  10771  expp1  10785  expcl2lemap  10790  expclzap  10803  expap0i  10810  nn0ltexp2  10948  bcval5  11002  hashinfuni  11016  hashennnuni  11018  hashnncl  11034  resunimafz0  11071  zfz1isolemiso  11079  zfz1isolem1  11080  zfz1iso  11081  wrdsymb0  11122  wrdlen1  11127  ccat1st1st  11193  swrdrlen  11214  pfxid  11239  pfxwrdsymbg  11243  pfxtrcfv  11246  pfxccat1  11255  pfxpfxid  11262  pfxcctswrd  11263  swrdccatin1  11278  pfxccatin12  11286  pfxccatid  11294  seq3shft  11370  cvg1nlemcau  11516  rexanuz  11520  resqrexlemoverl  11553  resqrexlemglsq  11554  resqrexlemsqa  11556  resqrexlemex  11557  rersqreu  11560  caubnd2  11649  maxleast  11745  fimaxre2  11759  minmax  11762  xrmaxiflemcl  11777  xrmaxiflemab  11779  xrmaxiflemlub  11780  xrmaxadd  11793  xrminmax  11797  xrbdtri  11808  climreu  11829  reccn2ap  11845  iserex  11871  climcvg1nlem  11881  serf0  11884  fz1f1o  11907  summodclem3  11912  zsumdc  11916  fsum3  11919  isumz  11921  isumss  11923  isumss2  11925  fsumsersdc  11927  fsum3ser  11929  fsumsplit  11939  isumclim2  11954  isumclim3  11955  fsum2dlemstep  11966  fsumcnv  11969  fisumcom2  11970  bcxmas  12021  isumle  12027  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  cvgratz  12064  mertenslemub  12066  mertenslemi1  12067  mertenslem2  12068  mertensabs  12069  zproddc  12111  prod1dc  12118  fprodsplitdc  12128  fprodsplit  12129  fprodunsn  12136  fprodcl2lem  12137  fprodcllemf  12145  fprod2dlemstep  12154  fprodcnv  12157  fprodcom2fi  12158  fprodle  12172  ef0lem  12192  fsumdvds  12374  mod2eq1n2dvds  12411  ndvdssub  12462  bitsfzolem  12486  bitsfzo  12487  bitsinv1  12494  gcdsupex  12499  gcdsupcl  12500  bezoutlemnewy  12538  bezoutlemmain  12540  bezoutlembi  12547  bezoutlemeu  12549  bezoutlemle  12550  uzwodc  12579  nnwofdc  12580  nnwosdc  12581  nninfctlemfo  12582  nninfct  12583  nn0seqcvgd  12584  eucalgf  12598  eucalginv  12599  lcmval  12606  prmind2  12663  dfphi2  12763  phiprmpw  12765  phimullem  12768  eulerthlem1  12770  eulerthlemrprm  12772  eulerthlema  12773  eulerthlemh  12774  eulerthlemth  12775  eulerth  12776  phisum  12784  odzcllem  12786  odzdvds  12789  pythagtriplem19  12826  pclemub  12831  pcprecl  12833  pceu  12839  pcqmul  12847  pcqcl  12850  pcxnn0cl  12854  pcxqcl  12856  pcge0  12857  pcdvdsb  12864  pceq0  12866  pcneg  12869  pcdvdstr  12871  pcgcd1  12872  pc2dvds  12874  pcz  12876  pcprmpw2  12877  pcaddlem  12883  pcadd  12884  pcmptcl  12886  pcmpt  12887  pcmptdvds  12889  fldivp1  12892  qexpz  12896  pockthlem  12900  pockthg  12901  prmunb  12906  1arith  12911  4sqlemffi  12940  4sqlem17  12951  4sqlem18  12952  4sqlem19  12953  ennnfonelemom  13000  ennnfoneleminc  13003  ennnfonelemhf1o  13005  ennnfonelemex  13006  ennnfonelemhom  13007  ennnfonelemdm  13012  ennnfonelemr  13015  ennnfonelemim  13016  exmidunben  13018  ctinfom  13020  inffinp1  13021  ctinf  13022  enctlem  13024  ctiunctlemu1st  13026  ctiunctlemu2nd  13027  ctiunctlemudc  13029  ctiunct  13032  ctiunctal  13033  unct  13034  ssomct  13037  nninfdclemcl  13040  nninfdclemp1  13042  nninfdc  13045  structcnvcnv  13069  setscom  13093  relelbasov  13116  ressbas2d  13122  ressval3d  13126  ressabsg  13130  restid2  13302  imasaddfnlemg  13368  quslem  13378  ercpbl  13385  fnpr2ob  13394  mgmplusf  13420  grpinvalem  13439  grpinva  13440  grprida  13441  fngsum  13442  igsumvalx  13443  gsum0g  13450  gsumval2  13451  ismnd  13473  mhmpropd  13520  grppropd  13571  grpsubf  13633  dfgrp3mlem  13652  mulgnn0p1  13691  mulgnn0subcl  13693  mulgsubcl  13694  mulgneg  13698  mulgnn0dir  13710  mulgnn0ass  13716  submmulg  13724  issubg2m  13747  issubg4m  13751  ghmmulg  13814  ghmrn  13815  lringuplu  14181  lmodscaf  14295  lssintclm  14369  lspun0  14410  lidlbas  14463  psr1clfi  14673  topontopon  14715  eltg3i  14751  epttop  14785  difopn  14803  uncld  14808  0nnei  14848  resttopon  14866  restabs  14870  restopnb  14876  lmcvg  14912  cnptopco  14917  cnss1  14921  cnss2  14922  cncnpi  14923  cncnp2m  14926  cnrest  14930  cnrest2  14931  cnrest2r  14932  cnptoprest  14934  cnptoprest2  14935  lmss  14941  lmff  14944  lmtopcnp  14945  lmcn  14946  txbasval  14962  upxp  14967  txcnmpt  14968  txdis1cn  14973  txlm  14974  lmcn2  14975  cnmpt11  14978  cnmpt11f  14979  cnmpt1t  14980  cnmpt12  14982  cnmpt21  14986  cnmpt21f  14987  cnmpt2t  14988  cnmpt22  14989  cnmpt22f  14990  cnmptcom  14993  hmeocnv  15002  hmeof1o  15004  hmeores  15010  txhmeo  15014  txswaphmeo  15016  isxmet2d  15043  blfvalps  15080  xblss2ps  15099  xblss2  15100  blfps  15104  blf  15105  unirnblps  15117  unirnbl  15118  isxms2  15147  bdxmet  15196  bdmet  15197  xmetxp  15202  xmettx  15205  blssioo  15248  tgioo  15249  mulcncflem  15302  divcncfap  15309  dedekindeulemuub  15312  dedekindeulemub  15313  dedekindeulemloc  15314  dedekindeulemlu  15316  suplociccreex  15319  suplociccex  15320  dedekindicclemuub  15321  dedekindicclemub  15322  dedekindicclemloc  15323  dedekindicclemlu  15325  dedekindicc  15328  ivthinclemlopn  15331  ivthinclemuopn  15333  ivthdich  15348  limcrcl  15353  limcmpted  15358  limccnp2lem  15371  limccnp2cntop  15372  limccoap  15373  dvrecap  15408  plyaddlem1  15442  plymullem1  15443  plycoeid3  15452  plyco  15454  plycj  15456  plyrecj  15458  dvply1  15460  dvply2g  15461  cosordlem  15544  logbgcd1irraplemexp  15663  logbgcd1irrap  15665  lgsneg1  15725  lgsdilem  15727  lgsdir2  15733  lgsdirprm  15734  lgsdir  15735  lgsne0  15738  lgsabs1  15739  lgsdirnn0  15747  lgsdinn0  15748  gausslemma2dlem1f1o  15760  gausslemma2dlem4  15764  lgseisenlem1  15770  lgsquadlem3  15779  2lgslem1a  15788  2sqlem5  15819  2sqlem7  15821  2sqlem8a  15822  2sqlem8  15823  2sqlem9  15824  gropeld  15871  grstructeld2dom  15872  uhgrm  15899  upgrm  15921  uhgredgm  15955  edgupgren  15960  edgumgren  15961  edgusgren  15982  ausgrusgrben  15987  umgr2edg1  16028  usgredg2vlem1  16041  uhgr0enedgfi  16055  vtxedgfi  16075  vtxlpfi  16076  vtxdumgrfival  16084  vtxd0nedgbfi  16085  wlkvtxm  16112  g0wlk0  16142  wlkres  16149  trlreslem  16158  clwwlkccatlem  16169  clwwlknnn  16181  bj-stand  16221  bj-charfundcALT  16281  bj-charfunbi  16283  bj-bdfindis  16419  bj-peano4  16427  strcollnfALT  16458  1dom1el  16463  2omap  16472  pw1map  16474  pwtrufal  16476  pwf1oexmid  16478  subctctexmid  16479  pw1nct  16482  nnsf  16485  nninfalllem1  16488  nninfall  16489  nninfsellemqall  16495  nnnninfen  16501  exmidsbthrlem  16504  sbthom  16508  cvgcmp2nlemabs  16514  trilpo  16525  iswomni0  16533  redcwlpo  16537  dceqnconst  16542  dcapnconst  16543  nconstwlpolem  16547  nconstwlpo  16548  neapmkvlem  16549  neapmkv  16550  ltlenmkv  16552  taupi  16555  alsi1d  16563  alsi2d  16564  alsc1d  16565  alsc2d  16566