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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylbb1  137  bicomd  141  pm5.74d  182  bitri  184  3imtr3i  200  ancomd  267  pm4.71d  397  pm4.71rd  398  imdistand  451  orcomd  741  3mix3  1199  mpjao3dan  1348  ecase23d  1391  exlimdh  1649  nexd  1666  alexnim  1701  excomim  1715  19.41  1738  equcomd  1759  nfexd  1814  sbh  1829  sbcof2  1863  sbidm  1904  sb6rf  1906  nfsbt  2036  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  eu2  2131  2euex  2174  eqcomd  2244  3eltr3g  2323  abbid  2355  neneqd  2441  eqnetrrid  2451  3netr3g  2454  necomd  2506  r19.21bi  2638  nrexdv  2643  rexlimd  2665  rabbidva  2809  elisset  2836  euind  3013  rmoan  3026  reuind  3031  2rmorex  3032  spsbc  3063  spesbc  3138  eldifad  3231  eldifbd  3232  3sstr3g  3290  sseqtrdi  3296  difindiss  3485  un00  3567  vvin  3569  undifss  3608  ifcldcd  3678  disjpr2  3773  difprsn1  3854  diftpsn3  3856  difsnss  3861  sneqr  3885  preqr1  3893  preq12b  3895  oprcl  3928  intab  3999  riinm  4085  rintm  4105  disjiun  4125  sndisj  4126  sn0disj  4127  3brtr3g  4164  trint  4246  iinexgm  4292  exmidexmid  4335  exmid01  4337  pwntru  4338  exmid1stab  4347  pwel  4360  exss  4369  0nelop  4390  euotd  4397  opelopabsb  4404  pwunim  4433  issod  4466  frind  4499  suctr  4568  orduniss  4572  onelini  4577  oneluni  4578  eusv2i  4603  rexxfrd  4611  rabxfrd  4617  reuhypd  4619  iunpw  4628  sucexg  4647  ordsucim  4649  ordtriexmidlem  4668  ontriexmidim  4671  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  ordsucunielexmid  4680  orddif  4696  suc11g  4706  onintexmid  4722  reg3exmidlemwe  4728  tfisi  4736  peano1  4743  peano2  4744  finds2  4750  omsinds  4771  brrelex12  4815  brel  4829  ssrel  4865  ssrel2  4867  ssrelrel  4877  elrel  4879  xpsspw  4889  relop  4932  dmxpm  5004  opelresi  5076  mptimass  5142  ndmima  5167  poirr2  5183  xpmlem  5211  xpimasn  5239  iotass  5358  iotacl  5365  dffun5r  5392  funeu  5405  funeu2  5406  funfnd  5411  funopg  5414  funun  5425  fununfun  5427  funinsn  5433  funtp  5437  funcnvuni  5453  funcnvres2  5459  imadiflem  5463  imadif  5464  funimaexglem  5467  fneu2  5491  fnimaeq0  5508  fnmpt  5513  ffrn  5548  fun2  5565  f00  5587  f0bi  5588  fimadmfo  5627  foimacnv  5660  resdif  5664  f1ococnv1  5671  fv3  5721  relelfvdm  5730  elfvm  5732  nfvres  5735  dffn5im  5751  mptfvex  5794  fvmptdf  5796  fvmptdv2  5798  fndmdif  5817  dff4im  5857  fmpt  5861  fmptd  5865  fmptdf  5868  f1oresrab  5876  fcoconst  5882  fsn  5883  funopsn  5894  ftpg  5902  fsnunf  5918  resfunexg  5939  mptmex  5948  isores1  6023  riota2df  6063  acexmidlemcase  6083  brabvv  6137  funoprabg  6190  fnovim  6200  ovmpodf  6223  ovi3  6229  elmpocl  6287  uchoice  6375  1stcof  6401  2ndcof  6402  opabn1stprc  6433  fnmpo  6442  fmpoco  6456  fo2ndf  6467  f1o2ndf1  6468  disjxp1  6476  fvdifsuppst  6488  fsuppeq  6491  fsuppeqg  6492  suppssrst  6505  suppssrgst  6506  brtpos2  6527  reldmtpos  6529  dftpos3  6538  dftpos4  6539  tpostpos2  6541  tposf2  6544  tposf12  6545  tposfo  6547  tposf  6548  smores2  6570  tfrlem1  6584  tfrlem3-2d  6588  tfrlemisucaccv  6601  tfrlemibxssdm  6603  tfrlemibfn  6604  tfrlemi1  6608  tfrexlem  6610  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfr1onlemaccex  6624  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemaccex  6637  tfrcldm  6639  rdgivallem  6657  rdgisucinc  6661  frecabex  6674  frecfnom  6677  frecfcllem  6680  frecsuclem  6682  omsuc  6750  nntri2  6772  nnsucuniel  6773  nnsseleq  6779  nnm00  6808  ecexr  6817  swoer  6840  elqsn0m  6882  iinerm  6886  erinxp  6888  ecinxp  6889  eroveu  6905  eroprf  6907  mapprc  6931  mapsn  6978  ixpprc  7007  ixp0  7019  resixp  7021  elixpsn  7023  dom2lem  7064  fundmen  7100  1dom1el  7113  dom0  7144  xpf1o  7150  mapxpen  7154  xpmapenlem  7155  ssenen  7158  nneneq  7164  ssfilem  7183  ssfilemd  7185  dif1en  7189  dif1enen  7190  fin0  7195  fin0or  7196  diffitest  7197  diffisn  7203  ac6sfi  7208  fimax2gtrilemstep  7211  fimax2gtri  7212  finexdc  7213  eqsndc  7216  exmidpweq  7222  pw1fin  7223  onunsnss  7230  unsnfidcel  7234  undifdcss  7236  undifdc  7237  tpfidceq  7243  fiintim  7244  fisseneq  7248  fidcenumlemr  7279  sbthlemi4  7284  sbthlemi5  7285  sbthlemi9  7289  fndmfifsupp  7304  fifo  7320  2omap  7325  suplubti  7347  supelti  7349  infmoti  7375  infisoti  7379  djulclb  7402  updjud  7429  omp1eomlem  7441  0ct  7454  ctmlemr  7455  ctssdclemn0  7457  ctssdccl  7458  ctssdc  7460  enumct  7462  nninfninc  7470  nnnninfeq2  7476  finomni  7487  fodjuomnilemdc  7491  fodjum  7493  fodjuomnilemres  7495  fodjumkvlemres  7506  omniwomnimkv  7514  nninfwlporlem  7520  nninfwlpoimlemginf  7523  nninfwlpoim  7526  nninfinfwlpo  7527  ficardon  7541  pr2cv1  7548  exmidonfinlem  7552  en2eleq  7554  exmidfodomrlemeldju  7558  exmidfodomrlemreseldju  7559  exmidfodomrlemim  7560  finacn  7567  acfun  7570  exmidaclem  7571  exmidontriimlem3  7586  exmidontriimlem4  7587  exmidontriim  7588  pw1if  7591  pw1on  7592  papsym  7619  papcotr  7620  dftap2  7624  2omotaplemst  7631  exmidapne  7633  ccfunen  7637  cc1  7638  cc2lem  7639  cc2  7640  cc3  7641  acnccim  7645  elni2  7688  indpi  7716  distrnqg  7761  subhalfnqq  7788  enq0sym  7806  enq0ref  7807  enq0tr  7808  nqnq0pi  7812  nnnq0lem1  7820  distrnq0  7833  elinp  7848  elnp1st2nd  7850  prltlu  7861  prnmaxl  7862  prnminu  7863  prarloc  7877  nqprm  7916  appdivnq  7937  prmuloc  7940  mullocpr  7945  distrlem4prl  7958  distrlem4pru  7959  ltexprlemm  7974  ltexprlemopl  7975  ltexprlemopu  7977  cauappcvgprlemopl  8020  cauappcvgprlemopu  8022  cauappcvgprlemdisj  8025  cauappcvgprlem2  8034  cauappcvgprlemlim  8035  caucvgprlemnkj  8040  caucvgprlemopl  8043  caucvgprlemopu  8045  caucvgprlemdisj  8048  caucvgprlemcl  8050  caucvgprlemladdfu  8051  caucvgprlemladdrl  8052  caucvgprlem2  8054  caucvgprprlemcbv  8061  caucvgprprlemval  8062  caucvgprprlemlol  8072  caucvgprprlemexbt  8080  caucvgprprlem1  8083  suplocexprlemrl  8091  suplocexprlemmu  8092  suplocexprlemru  8093  suplocexprlemdisj  8094  suplocexprlemloc  8095  suplocexprlemub  8097  suplocexprlemlub  8098  prsrlem1  8116  gt0srpr  8122  caucvgsrlemcl  8163  caucvgsrlembound  8168  caucvgsrlemgt1  8169  suplocsrlemb  8180  suplocsrlem  8182  suplocsr  8183  ltresr  8213  nnindnn  8267  axcaucvglemcl  8269  axcaucvglemval  8271  axcaucvglemcau  8272  axcaucvglemres  8273  axpre-suploclemres  8275  axpre-suploc  8276  sup3exmid  9296  indconst0  9312  indconst1  9313  nnind  9330  nn0supp  9629  nn0ge2m1nn  9637  zleloe  9701  zapne  9729  nn0lt2  9737  suprzclex  9755  zindd  9775  uzm1  9969  uzin  9971  infregelbex  10014  elnn1uz2  10023  nn01to3  10033  divfnzn  10037  qapne  10055  irraddap  10063  xrltnsym2  10213  xaddass  10288  xleadd1a  10292  xlt2add  10299  xlesubadd  10302  iooval2  10334  icoshftf1o  10410  fztri3or  10460  fzneuz  10525  4fvwrd4  10564  elfzo0  10610  infssuzex  10683  infssuzcldc  10685  infssfzcldc  10686  infssfzledc  10687  suprzubdc  10688  nninfdcex  10689  zsupssdc  10690  exbtwnzlemex  10701  ioom  10712  fzfig  10888  uzennn  10894  uzsinds  10902  iseqovex  10916  seq3val  10918  seqvalcd  10919  seqf  10922  seqovcd  10925  monoord2  10944  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  seq3f1olemqsum  10971  seq3f1o  10975  seqf1og  10979  seq3distr  10990  expp1  11004  expcl2lemap  11009  expclzap  11022  expap0i  11029  nn0ltexp2  11169  bcval5  11223  hashinfuni  11238  hashennnuni  11240  hashnncl  11256  resunimafz0  11296  hashf1lem2  11308  hashf1  11309  zfz1isolemiso  11313  zfz1isolem1  11314  zfz1iso  11315  wrdsymb0  11359  wrdlen1  11364  ccat1st1st  11431  swrdrlen  11455  pfxid  11480  pfxwrdsymbg  11484  pfxtrcfv  11487  pfxccat1  11496  pfxpfxid  11503  pfxcctswrd  11504  swrdccatin1  11519  pfxccatin12  11527  pfxccatid  11535  seq3shft  11625  cvg1nlemcau  11772  rexanuz  11776  resqrexlemoverl  11809  resqrexlemglsq  11810  resqrexlemsqa  11812  resqrexlemex  11813  rersqreu  11816  caubnd2  11906  maxleast  12002  fimaxre2  12016  minmax  12020  xrmaxiflemcl  12036  xrmaxiflemab  12038  xrmaxiflemlub  12039  xrmaxadd  12052  xrminmax  12056  xrbdtri  12067  climreu  12088  reccn2ap  12104  iserex  12130  climcvg1nlem  12140  serf0  12143  fz1f1o  12166  summodclem3  12172  zsumdc  12176  fsum3  12179  isumz  12181  isumss  12183  isumss2  12185  fsumsersdc  12187  fsum3ser  12189  fsumsplit  12199  isumclim2  12214  isumclim3  12215  fsum2dlemstep  12226  fsumcnv  12229  fisumcom2  12230  bcxmas  12281  isumle  12287  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  cvgratz  12324  mertenslemub  12326  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  zproddc  12371  prod1dc  12378  fprodsplitdc  12388  fprodsplit  12389  fprodunsn  12396  fprodcl2lem  12397  fprodcllemf  12405  fprod2dlemstep  12414  fprodcnv  12417  fprodcom2fi  12418  fprodle  12432  ef0lem  12452  fsumdvds  12634  mod2eq1n2dvds  12671  ndvdssub  12722  bitsfzolem  12746  bitsfzo  12747  bitsinv1  12754  gcdsupex  12759  gcdsupcl  12760  bezoutlemnewy  12798  bezoutlemmain  12800  bezoutlembi  12807  bezoutlemeu  12809  bezoutlemle  12810  uzwodc  12839  nnwofdc  12840  nnwosdc  12841  nninfctlemfo  12842  nninfct  12843  nn0seqcvgd  12844  eucalgf  12858  eucalginv  12859  lcmval  12866  prmind2  12923  dfphi2  13027  phiprmpw  13029  phimullem  13032  eulerthlem1  13034  eulerthlemrprm  13036  eulerthlema  13037  eulerthlemh  13038  eulerthlemth  13039  eulerth  13040  phisum  13048  odzcllem  13050  odzdvds  13053  pythagtriplem19  13090  pclemub  13095  pcprecl  13097  pceu  13103  pcqmul  13111  pcqcl  13114  pcxnn0cl  13118  pcxqcl  13120  pcge0  13121  pcdvdsb  13128  pceq0  13130  pcneg  13133  pcdvdstr  13135  pcgcd1  13136  pc2dvds  13138  pcz  13140  pcprmpw2  13141  pcaddlem  13147  pcadd  13148  pcmptcl  13150  pcmpt  13151  pcmptdvds  13153  fldivp1  13156  qexpz  13160  pockthlem  13164  pockthg  13165  prmunb  13170  1arith  13175  4sqlemffi  13204  4sqlem17  13215  4sqlem18  13216  4sqlem19  13217  prmlem1a  13250  ballotfilemcdc  13281  ballotfilem2  13286  ballotfilemfp1  13289  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemfmpn  13292  ballotfilemefi  13295  ballotfilemiex  13302  ballotfilemro  13324  ennnfonelemom  13357  ennnfoneleminc  13360  ennnfonelemhf1o  13362  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemdm  13369  ennnfonelemr  13372  ennnfonelemim  13373  exmidunben  13375  ctinfom  13377  inffinp1  13378  ctinf  13379  enctlem  13381  ctiunctlemu1st  13383  ctiunctlemu2nd  13384  ctiunctlemudc  13386  ctiunct  13389  ctiunctal  13390  unct  13391  ssomct  13394  nninfdclemcl  13397  nninfdclemp1  13399  nninfdc  13402  structcnvcnv  13426  setscom  13450  relelbasov  13474  ressbas2d  13481  ressval3d  13485  ressabsg  13489  restid2  13661  imasaddfnlemg  13694  quslem  13704  ercpbl  13711  fnpr2ob  13720  mgmplusf  13745  grpinvalem  13764  grpinva  13765  grprida  13766  fngzsum  13767  gzsumvalx  13768  gzsum0  13772  gzsumval2  13773  ismnd  13791  mhmpropd  13832  grppropd  13881  grpsubf  13943  dfgrp3mlem  13962  mulgnn0p1  13995  mulgnn0subcl  13997  mulgsubcl  13998  mulgneg  14002  mulgnn0dir  14014  mulgnn0ass  14020  submmulg  14028  issubg2m  14051  issubg4m  14055  ghmmulg  14118  ghmrn  14119  gsumvalfi  14242  gzsumgsum  14245  gsumf1ofi  14250  gsummptfidmsplit  14254  gsumresfi  14263  gsummhmfi  14264  gsumressfi  14267  gsum2d2fi  14274  gsumcom2fi  14275  lringuplu  14612  rrgsupp  14683  opprdrng  14729  lmodscaf  14756  lssintclm  14830  lspun0  14871  lidlbas  14924  psrbagconcl  15176  psrbagmax  15190  psrbagfsuppub  15192  gsumbagdiaglem  15194  psr1clfi  15218  mplsubgfilemcl  15246  mplsubgfileminv  15247  topontopon  15279  eltg3i  15315  epttop  15349  difopn  15367  uncld  15372  0nnei  15412  resttopon  15430  restabs  15434  restopnb  15440  lmcvg  15476  cnptopco  15481  cnss1  15485  cnss2  15486  cncnpi  15487  cncnp2m  15490  cnrest  15494  cnrest2  15495  cnrest2r  15496  cnptoprest  15498  cnptoprest2  15499  lmss  15505  lmff  15508  lmtopcnp  15509  lmcn  15510  txbasval  15526  upxp  15531  txcnmpt  15532  txdis1cn  15537  txlm  15538  lmcn2  15539  cnmpt11  15542  cnmpt11f  15543  cnmpt1t  15544  cnmpt12  15546  cnmpt21  15550  cnmpt21f  15551  cnmpt2t  15552  cnmpt22  15553  cnmpt22f  15554  cnmptcom  15557  hmeocnv  15566  hmeof1o  15568  hmeores  15574  txhmeo  15578  txswaphmeo  15580  isxmet2d  15607  blfvalps  15644  xblss2ps  15663  xblss2  15664  blfps  15668  blf  15669  unirnblps  15681  unirnbl  15682  isxms2  15711  bdxmet  15760  bdmet  15761  xmetxp  15766  xmettx  15769  blssioo  15812  tgioo  15813  mulcncflem  15866  divcncfap  15873  dedekindeulemuub  15876  dedekindeulemub  15877  dedekindeulemloc  15878  dedekindeulemlu  15880  suplociccreex  15883  suplociccex  15884  dedekindicclemuub  15885  dedekindicclemub  15886  dedekindicclemloc  15887  dedekindicclemlu  15889  dedekindicc  15892  ivthinclemlopn  15895  ivthinclemuopn  15897  ivthdich  15912  limcrcl  15917  limcmpted  15922  limccnp2lem  15935  limccnp2cntop  15936  limccoap  15937  dvrecap  15972  plyaddlem1  16006  plymullem1  16007  plycoeid3  16016  plyco  16018  plycj  16020  plyrecj  16022  dvply1  16024  dvply2g  16025  cosordlem  16110  logbgcd1irraplemexp  16237  logbgcd1irrap  16239  zprmlogbaplem2  16249  zprmlogbaplem3  16250  birthdaylem2  16259  birthdaylem3  16260  chtqge0  16280  ppiprm  16292  ppinprm  16293  chtprm  16294  chtnprm  16295  chtqwordi  16296  ppiqltx  16314  bposlem2  16345  lgsneg1  16382  lgsdilem  16384  lgsdir2  16390  lgsdirprm  16391  lgsdir  16392  lgsne0  16395  lgsabs1  16396  lgsdirnn0  16404  lgsdinn0  16405  gausslemma2dlem1f1o  16417  gausslemma2dlem4  16421  lgseisenlem1  16427  lgsquadlem3  16436  2lgslem1a  16445  2sqlem5  16476  2sqlem7  16478  2sqlem8a  16479  2sqlem8  16480  2sqlem9  16481  gropeld  16528  grstructeld2dom  16529  uhgrm  16557  upgrm  16579  upgr1een  16603  uhgredgm  16615  edgupgren  16620  edgumgren  16621  edgusgren  16642  ausgrusgrben  16647  umgr2edg1  16688  usgredg2vlem1  16701  uhgr0enedgfi  16715  subupgr  16752  vtxedgfi  16768  vtxlpfi  16769  vtxdumgrfival  16777  vtxd0nedgbfi  16778  1hevtxdg0fi  16786  p1evtxdeqfilem  16790  wlkvtxm  16819  g0wlk0  16849  wlkres  16858  trlreslem  16868  clwwlkccatlem  16879  clwwlknnn  16891  trlsegvdeglem6  16944  eupth2lem3lem3fi  16949  eupth2lem3lem7fi  16953  eulerpathum  16960  dichmul0or  16998  bj-stand  17014  bj-charfundcALT  17073  bj-charfunbi  17075  bj-bdfindis  17211  bj-peano4  17219  strcollnfALT  17250  pw1map  17263  pwtrufal  17265  pwf1oexmid  17267  subctctexmid  17268  pw1nct  17271  stnot  17277  wexmiddc  17280  nnsf  17287  nninfalllem1  17290  nninfall  17291  nninfsellemqall  17297  nnnninfen  17303  exmidsbthrlem  17306  sbthom  17310  repiecef  17316  cvgcmp2nlemabs  17320  trilpo  17332  iswomni0  17341  redcwlpo  17345  dceqnconst  17350  dcapnconst  17351  nconstwlpolem  17355  nconstwlpo  17356  neapmkvlem  17357  neapmkv  17358  ltlenmkv  17360  taupi  17363  als1d  17373  als2d  17374  rals1d  17375  rals2d  17376  alseu1d  17409  alseu2d  17410  ralseu1d  17411  ralseu2d  17412  dfalseu2  17417