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  4238  exmidexmid  4280  exmid01  4282  pwntru  4283  exmid1stab  4292  pwel  4304  exss  4313  0nelop  4334  euotd  4341  opelopabsb  4348  pwunim  4377  issod  4410  frind  4443  suctr  4512  orduniss  4516  onelini  4521  oneluni  4522  eusv2i  4546  rexxfrd  4554  rabxfrd  4560  reuhypd  4562  iunpw  4571  sucexg  4590  ordsucim  4592  ordtriexmidlem  4611  ontriexmidim  4614  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  ordsucunielexmid  4623  orddif  4639  suc11g  4649  onintexmid  4665  reg3exmidlemwe  4671  tfisi  4679  peano1  4686  peano2  4687  finds2  4693  omsinds  4714  brrelex12  4757  brel  4771  ssrel  4807  ssrel2  4809  ssrelrel  4819  elrel  4821  xpsspw  4831  relop  4872  dmxpm  4944  opelresi  5016  mptimass  5081  ndmima  5105  poirr2  5121  xpmlem  5149  xpimasn  5177  iotass  5296  iotacl  5303  dffun5r  5330  funeu  5343  funeu2  5344  funfnd  5349  funopg  5352  funun  5362  fununfun  5364  funinsn  5370  funtp  5374  funcnvuni  5390  funcnvres2  5396  imadiflem  5400  imadif  5401  funimaexglem  5404  fneu2  5428  fnimaeq0  5445  fnmpt  5450  fun2  5498  f00  5517  f0bi  5518  fimadmfo  5557  foimacnv  5590  resdif  5594  f1ococnv1  5601  fv3  5650  relelfvdm  5659  elfvm  5660  nfvres  5663  dffn5im  5679  mptfvex  5720  fvmptdf  5722  fvmptdv2  5724  fndmdif  5740  dff4im  5781  fmpt  5785  fmptd  5789  fmptdf  5792  f1oresrab  5800  fcoconst  5806  fsn  5807  funopsn  5817  ftpg  5823  fsnunf  5839  resfunexg  5860  isores1  5938  riota2df  5976  acexmidlemcase  5996  brabvv  6050  funoprabg  6103  fnovim  6113  ovmpodf  6136  ovi3  6142  elmpocl  6200  uchoice  6283  1stcof  6309  2ndcof  6310  fnmpo  6348  fmpoco  6362  fo2ndf  6373  f1o2ndf1  6374  disjxp1  6382  brtpos2  6397  reldmtpos  6399  dftpos3  6408  dftpos4  6409  tpostpos2  6411  tposf2  6414  tposf12  6415  tposfo  6417  tposf  6418  smores2  6440  tfrlem1  6454  tfrlem3-2d  6458  tfrlemisucaccv  6471  tfrlemibxssdm  6473  tfrlemibfn  6474  tfrlemi1  6478  tfrexlem  6480  tfr1onlemsucaccv  6487  tfr1onlembxssdm  6489  tfr1onlembfn  6490  tfr1onlemaccex  6494  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllembfn  6503  tfrcllemaccex  6507  tfrcldm  6509  rdgivallem  6527  rdgisucinc  6531  frecabex  6544  frecfnom  6547  frecfcllem  6550  frecsuclem  6552  omsuc  6618  nntri2  6640  nnsucuniel  6641  nnsseleq  6647  nnm00  6676  ecexr  6685  swoer  6708  elqsn0m  6750  iinerm  6754  erinxp  6756  ecinxp  6757  eroveu  6773  eroprf  6775  mapprc  6799  mapsn  6837  ixpprc  6866  ixp0  6878  resixp  6880  elixpsn  6882  dom2lem  6923  fundmen  6959  dom0  6999  xpf1o  7005  mapxpen  7009  xpmapenlem  7010  ssenen  7012  nneneq  7018  ssfilem  7037  dif1en  7041  dif1enen  7042  fin0  7047  fin0or  7048  diffitest  7049  diffisn  7055  ac6sfi  7060  fimax2gtrilemstep  7062  fimax2gtri  7063  finexdc  7064  exmidpweq  7071  pw1fin  7072  onunsnss  7079  unsnfidcel  7083  undifdcss  7085  undifdc  7086  tpfidceq  7092  fiintim  7093  fisseneq  7096  fidcenumlemr  7122  sbthlemi4  7127  sbthlemi5  7128  sbthlemi9  7132  fifo  7147  suplubti  7167  supelti  7169  infmoti  7195  infisoti  7199  djulclb  7222  updjud  7249  omp1eomlem  7261  0ct  7274  ctmlemr  7275  ctssdclemn0  7277  ctssdccl  7278  ctssdc  7280  enumct  7282  nninfninc  7290  nnnninfeq2  7296  finomni  7307  fodjuomnilemdc  7311  fodjum  7313  fodjuomnilemres  7315  fodjumkvlemres  7326  omniwomnimkv  7334  nninfwlporlem  7340  nninfwlpoimlemginf  7343  nninfwlpoim  7346  nninfinfwlpo  7347  ficardon  7361  pr2cv1  7368  exmidonfinlem  7371  en2eleq  7373  exmidfodomrlemeldju  7377  exmidfodomrlemreseldju  7378  exmidfodomrlemim  7379  finacn  7386  acfun  7389  exmidaclem  7390  exmidontriimlem3  7405  exmidontriimlem4  7406  exmidontriim  7407  pw1if  7410  pw1on  7411  dftap2  7437  2omotaplemst  7444  exmidapne  7446  ccfunen  7450  cc1  7451  cc2lem  7452  cc2  7453  cc3  7454  acnccim  7458  elni2  7501  indpi  7529  distrnqg  7574  subhalfnqq  7601  enq0sym  7619  enq0ref  7620  enq0tr  7621  nqnq0pi  7625  nnnq0lem1  7633  distrnq0  7646  elinp  7661  elnp1st2nd  7663  prltlu  7674  prnmaxl  7675  prnminu  7676  prarloc  7690  nqprm  7729  appdivnq  7750  prmuloc  7753  mullocpr  7758  distrlem4prl  7771  distrlem4pru  7772  ltexprlemm  7787  ltexprlemopl  7788  ltexprlemopu  7790  cauappcvgprlemopl  7833  cauappcvgprlemopu  7835  cauappcvgprlemdisj  7838  cauappcvgprlem2  7847  cauappcvgprlemlim  7848  caucvgprlemnkj  7853  caucvgprlemopl  7856  caucvgprlemopu  7858  caucvgprlemdisj  7861  caucvgprlemcl  7863  caucvgprlemladdfu  7864  caucvgprlemladdrl  7865  caucvgprlem2  7867  caucvgprprlemcbv  7874  caucvgprprlemval  7875  caucvgprprlemlol  7885  caucvgprprlemexbt  7893  caucvgprprlem1  7896  suplocexprlemrl  7904  suplocexprlemmu  7905  suplocexprlemru  7906  suplocexprlemdisj  7907  suplocexprlemloc  7908  suplocexprlemub  7910  suplocexprlemlub  7911  prsrlem1  7929  gt0srpr  7935  caucvgsrlemcl  7976  caucvgsrlembound  7981  caucvgsrlemgt1  7982  suplocsrlemb  7993  suplocsrlem  7995  suplocsr  7996  ltresr  8026  nnindnn  8080  axcaucvglemcl  8082  axcaucvglemval  8084  axcaucvglemcau  8085  axcaucvglemres  8086  axpre-suploclemres  8088  axpre-suploc  8089  sup3exmid  9104  nnind  9126  nn0supp  9421  nn0ge2m1nn  9429  zleloe  9493  zapne  9521  nn0lt2  9528  suprzclex  9545  zindd  9565  uzm1  9753  uzin  9755  infregelbex  9793  elnn1uz2  9802  nn01to3  9812  divfnzn  9816  qapne  9834  xrltnsym2  9990  xaddass  10065  xleadd1a  10069  xlt2add  10076  xlesubadd  10079  iooval2  10111  icoshftf1o  10187  fztri3or  10235  fzneuz  10297  4fvwrd4  10336  elfzo0  10382  infssuzex  10453  infssuzcldc  10455  suprzubdc  10456  nninfdcex  10457  zsupssdc  10458  exbtwnzlemex  10469  ioom  10480  fzfig  10652  uzennn  10658  uzsinds  10666  iseqovex  10680  seq3val  10682  seqvalcd  10683  seqf  10686  seqovcd  10689  monoord2  10708  iseqf1olemjpcl  10730  iseqf1olemqpcl  10731  seq3f1olemqsum  10735  seq3f1o  10739  seqf1og  10743  seq3distr  10754  expp1  10768  expcl2lemap  10773  expclzap  10786  expap0i  10793  nn0ltexp2  10931  bcval5  10985  hashinfuni  10999  hashennnuni  11001  hashnncl  11017  resunimafz0  11053  zfz1isolemiso  11061  zfz1isolem1  11062  zfz1iso  11063  wrdsymb0  11104  wrdlen1  11109  ccat1st1st  11172  swrdrlen  11193  pfxid  11218  pfxwrdsymbg  11222  pfxtrcfv  11225  pfxccat1  11234  pfxpfxid  11241  pfxcctswrd  11242  swrdccatin1  11257  pfxccatin12  11265  pfxccatid  11273  seq3shft  11349  cvg1nlemcau  11495  rexanuz  11499  resqrexlemoverl  11532  resqrexlemglsq  11533  resqrexlemsqa  11535  resqrexlemex  11536  rersqreu  11539  caubnd2  11628  maxleast  11724  fimaxre2  11738  minmax  11741  xrmaxiflemcl  11756  xrmaxiflemab  11758  xrmaxiflemlub  11759  xrmaxadd  11772  xrminmax  11776  xrbdtri  11787  climreu  11808  reccn2ap  11824  iserex  11850  climcvg1nlem  11860  serf0  11863  fz1f1o  11886  summodclem3  11891  zsumdc  11895  fsum3  11898  isumz  11900  isumss  11902  isumss2  11904  fsumsersdc  11906  fsum3ser  11908  fsumsplit  11918  isumclim2  11933  isumclim3  11934  fsum2dlemstep  11945  fsumcnv  11948  fisumcom2  11949  bcxmas  12000  isumle  12006  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  cvgratz  12043  mertenslemub  12045  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  zproddc  12090  prod1dc  12097  fprodsplitdc  12107  fprodsplit  12108  fprodunsn  12115  fprodcl2lem  12116  fprodcllemf  12124  fprod2dlemstep  12133  fprodcnv  12136  fprodcom2fi  12137  fprodle  12151  ef0lem  12171  fsumdvds  12353  mod2eq1n2dvds  12390  ndvdssub  12441  bitsfzolem  12465  bitsfzo  12466  bitsinv1  12473  gcdsupex  12478  gcdsupcl  12479  bezoutlemnewy  12517  bezoutlemmain  12519  bezoutlembi  12526  bezoutlemeu  12528  bezoutlemle  12529  uzwodc  12558  nnwofdc  12559  nnwosdc  12560  nninfctlemfo  12561  nninfct  12562  nn0seqcvgd  12563  eucalgf  12577  eucalginv  12578  lcmval  12585  prmind2  12642  dfphi2  12742  phiprmpw  12744  phimullem  12747  eulerthlem1  12749  eulerthlemrprm  12751  eulerthlema  12752  eulerthlemh  12753  eulerthlemth  12754  eulerth  12755  phisum  12763  odzcllem  12765  odzdvds  12768  pythagtriplem19  12805  pclemub  12810  pcprecl  12812  pceu  12818  pcqmul  12826  pcqcl  12829  pcxnn0cl  12833  pcxqcl  12835  pcge0  12836  pcdvdsb  12843  pceq0  12845  pcneg  12848  pcdvdstr  12850  pcgcd1  12851  pc2dvds  12853  pcz  12855  pcprmpw2  12856  pcaddlem  12862  pcadd  12863  pcmptcl  12865  pcmpt  12866  pcmptdvds  12868  fldivp1  12871  qexpz  12875  pockthlem  12879  pockthg  12880  prmunb  12885  1arith  12890  4sqlemffi  12919  4sqlem17  12930  4sqlem18  12931  4sqlem19  12932  ennnfonelemom  12979  ennnfoneleminc  12982  ennnfonelemhf1o  12984  ennnfonelemex  12985  ennnfonelemhom  12986  ennnfonelemdm  12991  ennnfonelemr  12994  ennnfonelemim  12995  exmidunben  12997  ctinfom  12999  inffinp1  13000  ctinf  13001  enctlem  13003  ctiunctlemu1st  13005  ctiunctlemu2nd  13006  ctiunctlemudc  13008  ctiunct  13011  ctiunctal  13012  unct  13013  ssomct  13016  nninfdclemcl  13019  nninfdclemp1  13021  nninfdc  13024  structcnvcnv  13048  setscom  13072  relelbasov  13095  ressbas2d  13101  ressval3d  13105  ressabsg  13109  restid2  13281  imasaddfnlemg  13347  quslem  13357  ercpbl  13364  fnpr2ob  13373  mgmplusf  13399  grpinvalem  13418  grpinva  13419  grprida  13420  fngsum  13421  igsumvalx  13422  gsum0g  13429  gsumval2  13430  ismnd  13452  mhmpropd  13499  grppropd  13550  grpsubf  13612  dfgrp3mlem  13631  mulgnn0p1  13670  mulgnn0subcl  13672  mulgsubcl  13673  mulgneg  13677  mulgnn0dir  13689  mulgnn0ass  13695  submmulg  13703  issubg2m  13726  issubg4m  13730  ghmmulg  13793  ghmrn  13794  lringuplu  14160  lmodscaf  14274  lssintclm  14348  lspun0  14389  lidlbas  14442  psr1clfi  14652  topontopon  14694  eltg3i  14730  epttop  14764  difopn  14782  uncld  14787  0nnei  14827  resttopon  14845  restabs  14849  restopnb  14855  lmcvg  14891  cnptopco  14896  cnss1  14900  cnss2  14901  cncnpi  14902  cncnp2m  14905  cnrest  14909  cnrest2  14910  cnrest2r  14911  cnptoprest  14913  cnptoprest2  14914  lmss  14920  lmff  14923  lmtopcnp  14924  lmcn  14925  txbasval  14941  upxp  14946  txcnmpt  14947  txdis1cn  14952  txlm  14953  lmcn2  14954  cnmpt11  14957  cnmpt11f  14958  cnmpt1t  14959  cnmpt12  14961  cnmpt21  14965  cnmpt21f  14966  cnmpt2t  14967  cnmpt22  14968  cnmpt22f  14969  cnmptcom  14972  hmeocnv  14981  hmeof1o  14983  hmeores  14989  txhmeo  14993  txswaphmeo  14995  isxmet2d  15022  blfvalps  15059  xblss2ps  15078  xblss2  15079  blfps  15083  blf  15084  unirnblps  15096  unirnbl  15097  isxms2  15126  bdxmet  15175  bdmet  15176  xmetxp  15181  xmettx  15184  blssioo  15227  tgioo  15228  mulcncflem  15281  divcncfap  15288  dedekindeulemuub  15291  dedekindeulemub  15292  dedekindeulemloc  15293  dedekindeulemlu  15295  suplociccreex  15298  suplociccex  15299  dedekindicclemuub  15300  dedekindicclemub  15301  dedekindicclemloc  15302  dedekindicclemlu  15304  dedekindicc  15307  ivthinclemlopn  15310  ivthinclemuopn  15312  ivthdich  15327  limcrcl  15332  limcmpted  15337  limccnp2lem  15350  limccnp2cntop  15351  limccoap  15352  dvrecap  15387  plyaddlem1  15421  plymullem1  15422  plycoeid3  15431  plyco  15433  plycj  15435  plyrecj  15437  dvply1  15439  dvply2g  15440  cosordlem  15523  logbgcd1irraplemexp  15642  logbgcd1irrap  15644  lgsneg1  15704  lgsdilem  15706  lgsdir2  15712  lgsdirprm  15713  lgsdir  15714  lgsne0  15717  lgsabs1  15718  lgsdirnn0  15726  lgsdinn0  15727  gausslemma2dlem1f1o  15739  gausslemma2dlem4  15743  lgseisenlem1  15749  lgsquadlem3  15758  2lgslem1a  15767  2sqlem5  15798  2sqlem7  15800  2sqlem8a  15801  2sqlem8  15802  2sqlem9  15803  gropeld  15850  grstructeld2dom  15851  uhgrm  15878  upgrm  15900  uhgredgm  15934  edgupgren  15939  edgumgren  15940  edgusgren  15961  ausgrusgrben  15966  umgr2edg1  16007  usgredg2vlem1  16020  g0wlk0  16081  bj-stand  16112  bj-charfundcALT  16172  bj-charfunbi  16174  bj-bdfindis  16310  bj-peano4  16318  strcollnfALT  16349  1dom1el  16354  2omap  16359  pw1map  16361  pwtrufal  16363  pwf1oexmid  16365  subctctexmid  16366  pw1nct  16369  nnsf  16371  nninfalllem1  16374  nninfall  16375  nninfsellemqall  16381  nnnninfen  16387  exmidsbthrlem  16390  sbthom  16394  cvgcmp2nlemabs  16400  trilpo  16411  iswomni0  16419  redcwlpo  16423  dceqnconst  16428  dcapnconst  16429  nconstwlpolem  16433  nconstwlpo  16434  neapmkvlem  16435  neapmkv  16436  ltlenmkv  16438  taupi  16441  alsi1d  16449  alsi2d  16450  alsc1d  16451  alsc2d  16452