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  3brtr3g  4163  trint  4244  iinexgm  4290  exmidexmid  4333  exmid01  4335  pwntru  4336  exmid1stab  4345  pwel  4358  exss  4367  0nelop  4388  euotd  4395  opelopabsb  4402  pwunim  4431  issod  4464  frind  4497  suctr  4566  orduniss  4570  onelini  4575  oneluni  4576  eusv2i  4601  rexxfrd  4609  rabxfrd  4615  reuhypd  4617  iunpw  4626  sucexg  4645  ordsucim  4647  ordtriexmidlem  4666  ontriexmidim  4669  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  ordsucunielexmid  4678  orddif  4694  suc11g  4704  onintexmid  4720  reg3exmidlemwe  4726  tfisi  4734  peano1  4741  peano2  4742  finds2  4748  omsinds  4769  brrelex12  4813  brel  4827  ssrel  4863  ssrel2  4865  ssrelrel  4875  elrel  4877  xpsspw  4887  relop  4930  dmxpm  5002  opelresi  5074  mptimass  5139  ndmima  5164  poirr2  5180  xpmlem  5208  xpimasn  5236  iotass  5355  iotacl  5362  dffun5r  5389  funeu  5402  funeu2  5403  funfnd  5408  funopg  5411  funun  5422  fununfun  5424  funinsn  5430  funtp  5434  funcnvuni  5450  funcnvres2  5456  imadiflem  5460  imadif  5461  funimaexglem  5464  fneu2  5488  fnimaeq0  5505  fnmpt  5510  ffrn  5545  fun2  5562  f00  5584  f0bi  5585  fimadmfo  5624  foimacnv  5657  resdif  5661  f1ococnv1  5668  fv3  5718  relelfvdm  5727  elfvm  5729  nfvres  5732  dffn5im  5748  mptfvex  5791  fvmptdf  5793  fvmptdv2  5795  fndmdif  5814  dff4im  5854  fmpt  5858  fmptd  5862  fmptdf  5865  f1oresrab  5873  fcoconst  5879  fsn  5880  funopsn  5891  ftpg  5899  fsnunf  5915  resfunexg  5936  mptmex  5945  isores1  6020  riota2df  6060  acexmidlemcase  6080  brabvv  6134  funoprabg  6187  fnovim  6197  ovmpodf  6220  ovi3  6226  elmpocl  6284  uchoice  6371  1stcof  6397  2ndcof  6398  opabn1stprc  6429  fnmpo  6438  fmpoco  6452  fo2ndf  6463  f1o2ndf1  6464  disjxp1  6472  fvdifsuppst  6484  fsuppeq  6487  fsuppeqg  6488  suppssrst  6501  suppssrgst  6502  brtpos2  6522  reldmtpos  6524  dftpos3  6533  dftpos4  6534  tpostpos2  6536  tposf2  6539  tposf12  6540  tposfo  6542  tposf  6543  smores2  6565  tfrlem1  6579  tfrlem3-2d  6583  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemi1  6603  tfrexlem  6605  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemaccex  6619  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemaccex  6632  tfrcldm  6634  rdgivallem  6652  rdgisucinc  6656  frecabex  6669  frecfnom  6672  frecfcllem  6675  frecsuclem  6677  omsuc  6745  nntri2  6767  nnsucuniel  6768  nnsseleq  6774  nnm00  6803  ecexr  6812  swoer  6835  elqsn0m  6877  iinerm  6881  erinxp  6883  ecinxp  6884  eroveu  6900  eroprf  6902  mapprc  6926  mapsn  6972  ixpprc  7001  ixp0  7013  resixp  7015  elixpsn  7017  dom2lem  7058  fundmen  7094  1dom1el  7107  dom0  7138  xpf1o  7144  mapxpen  7148  xpmapenlem  7149  ssenen  7152  nneneq  7158  ssfilem  7177  ssfilemd  7179  dif1en  7183  dif1enen  7184  fin0  7189  fin0or  7190  diffitest  7191  diffisn  7197  ac6sfi  7202  fimax2gtrilemstep  7205  fimax2gtri  7206  finexdc  7207  eqsndc  7210  exmidpweq  7216  pw1fin  7217  onunsnss  7224  unsnfidcel  7228  undifdcss  7230  undifdc  7231  tpfidceq  7237  fiintim  7238  fisseneq  7242  fidcenumlemr  7272  sbthlemi4  7277  sbthlemi5  7278  sbthlemi9  7282  fifo  7314  2omap  7319  suplubti  7341  supelti  7343  infmoti  7369  infisoti  7373  djulclb  7396  updjud  7423  omp1eomlem  7435  0ct  7448  ctmlemr  7449  ctssdclemn0  7451  ctssdccl  7452  ctssdc  7454  enumct  7456  nninfninc  7464  nnnninfeq2  7470  finomni  7481  fodjuomnilemdc  7485  fodjum  7487  fodjuomnilemres  7489  fodjumkvlemres  7500  omniwomnimkv  7508  nninfwlporlem  7514  nninfwlpoimlemginf  7517  nninfwlpoim  7520  nninfinfwlpo  7521  ficardon  7535  pr2cv1  7542  exmidonfinlem  7546  en2eleq  7548  exmidfodomrlemeldju  7552  exmidfodomrlemreseldju  7553  exmidfodomrlemim  7554  finacn  7561  acfun  7564  exmidaclem  7565  exmidontriimlem3  7580  exmidontriimlem4  7581  exmidontriim  7582  pw1if  7585  pw1on  7586  papsym  7613  papcotr  7614  dftap2  7618  2omotaplemst  7625  exmidapne  7627  ccfunen  7631  cc1  7632  cc2lem  7633  cc2  7634  cc3  7635  acnccim  7639  elni2  7682  indpi  7710  distrnqg  7755  subhalfnqq  7782  enq0sym  7800  enq0ref  7801  enq0tr  7802  nqnq0pi  7806  nnnq0lem1  7814  distrnq0  7827  elinp  7842  elnp1st2nd  7844  prltlu  7855  prnmaxl  7856  prnminu  7857  prarloc  7871  nqprm  7910  appdivnq  7931  prmuloc  7934  mullocpr  7939  distrlem4prl  7952  distrlem4pru  7953  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemopu  7971  cauappcvgprlemopl  8014  cauappcvgprlemopu  8016  cauappcvgprlemdisj  8019  cauappcvgprlem2  8028  cauappcvgprlemlim  8029  caucvgprlemnkj  8034  caucvgprlemopl  8037  caucvgprlemopu  8039  caucvgprlemdisj  8042  caucvgprlemcl  8044  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprlem2  8048  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemlol  8066  caucvgprprlemexbt  8074  caucvgprprlem1  8077  suplocexprlemrl  8085  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemub  8091  suplocexprlemlub  8092  prsrlem1  8110  gt0srpr  8116  caucvgsrlemcl  8157  caucvgsrlembound  8162  caucvgsrlemgt1  8163  suplocsrlemb  8174  suplocsrlem  8176  suplocsr  8177  ltresr  8207  nnindnn  8261  axcaucvglemcl  8263  axcaucvglemval  8265  axcaucvglemcau  8266  axcaucvglemres  8267  axpre-suploclemres  8269  axpre-suploc  8270  sup3exmid  9290  indconst0  9305  indconst1  9306  nnind  9323  nn0supp  9624  nn0ge2m1nn  9632  zleloe  9696  zapne  9724  nn0lt2  9732  suprzclex  9749  zindd  9769  uzm1  9963  uzin  9965  infregelbex  10008  elnn1uz2  10017  nn01to3  10027  divfnzn  10031  qapne  10049  irraddap  10057  xrltnsym2  10207  xaddass  10282  xleadd1a  10286  xlt2add  10293  xlesubadd  10296  iooval2  10328  icoshftf1o  10404  fztri3or  10454  fzneuz  10519  4fvwrd4  10558  elfzo0  10604  infssuzex  10677  infssuzcldc  10679  infssfzcldc  10680  infssfzledc  10681  suprzubdc  10682  nninfdcex  10683  zsupssdc  10684  exbtwnzlemex  10695  ioom  10706  fzfig  10881  uzennn  10887  uzsinds  10895  iseqovex  10909  seq3val  10911  seqvalcd  10912  seqf  10915  seqovcd  10918  monoord2  10937  iseqf1olemjpcl  10959  iseqf1olemqpcl  10960  seq3f1olemqsum  10964  seq3f1o  10968  seqf1og  10972  seq3distr  10983  expp1  10997  expcl2lemap  11002  expclzap  11015  expap0i  11022  nn0ltexp2  11162  bcval5  11216  hashinfuni  11231  hashennnuni  11233  hashnncl  11249  resunimafz0  11289  hashf1lem2  11301  hashf1  11302  zfz1isolemiso  11306  zfz1isolem1  11307  zfz1iso  11308  wrdsymb0  11352  wrdlen1  11357  ccat1st1st  11424  swrdrlen  11448  pfxid  11473  pfxwrdsymbg  11477  pfxtrcfv  11480  pfxccat1  11489  pfxpfxid  11496  pfxcctswrd  11497  swrdccatin1  11512  pfxccatin12  11520  pfxccatid  11528  seq3shft  11618  cvg1nlemcau  11765  rexanuz  11769  resqrexlemoverl  11802  resqrexlemglsq  11803  resqrexlemsqa  11805  resqrexlemex  11806  rersqreu  11809  caubnd2  11899  maxleast  11995  fimaxre2  12009  minmax  12013  xrmaxiflemcl  12029  xrmaxiflemab  12031  xrmaxiflemlub  12032  xrmaxadd  12045  xrminmax  12049  xrbdtri  12060  climreu  12081  reccn2ap  12097  iserex  12123  climcvg1nlem  12133  serf0  12136  fz1f1o  12159  summodclem3  12165  zsumdc  12169  fsum3  12172  isumz  12174  isumss  12176  isumss2  12178  fsumsersdc  12180  fsum3ser  12182  fsumsplit  12192  isumclim2  12207  isumclim3  12208  fsum2dlemstep  12219  fsumcnv  12222  fisumcom2  12223  bcxmas  12274  isumle  12280  cvgratnnlemnexp  12309  cvgratnnlemmn  12310  cvgratz  12317  mertenslemub  12319  mertenslemi1  12320  mertenslem2  12321  mertensabs  12322  zproddc  12364  prod1dc  12371  fprodsplitdc  12381  fprodsplit  12382  fprodunsn  12389  fprodcl2lem  12390  fprodcllemf  12398  fprod2dlemstep  12407  fprodcnv  12410  fprodcom2fi  12411  fprodle  12425  ef0lem  12445  fsumdvds  12627  mod2eq1n2dvds  12664  ndvdssub  12715  bitsfzolem  12739  bitsfzo  12740  bitsinv1  12747  gcdsupex  12752  gcdsupcl  12753  bezoutlemnewy  12791  bezoutlemmain  12793  bezoutlembi  12800  bezoutlemeu  12802  bezoutlemle  12803  uzwodc  12832  nnwofdc  12833  nnwosdc  12834  nninfctlemfo  12835  nninfct  12836  nn0seqcvgd  12837  eucalgf  12851  eucalginv  12852  lcmval  12859  prmind2  12916  dfphi2  13020  phiprmpw  13022  phimullem  13025  eulerthlem1  13027  eulerthlemrprm  13029  eulerthlema  13030  eulerthlemh  13031  eulerthlemth  13032  eulerth  13033  phisum  13041  odzcllem  13043  odzdvds  13046  pythagtriplem19  13083  pclemub  13088  pcprecl  13090  pceu  13096  pcqmul  13104  pcqcl  13107  pcxnn0cl  13111  pcxqcl  13113  pcge0  13114  pcdvdsb  13121  pceq0  13123  pcneg  13126  pcdvdstr  13128  pcgcd1  13129  pc2dvds  13131  pcz  13133  pcprmpw2  13134  pcaddlem  13140  pcadd  13141  pcmptcl  13143  pcmpt  13144  pcmptdvds  13146  fldivp1  13149  qexpz  13153  pockthlem  13157  pockthg  13158  prmunb  13163  1arith  13168  4sqlemffi  13197  4sqlem17  13208  4sqlem18  13209  4sqlem19  13210  prmlem1a  13243  ballotfilemcdc  13274  ballotfilem2  13279  ballotfilemfp1  13282  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemfmpn  13285  ballotfilemefi  13288  ballotfilemiex  13295  ballotfilemro  13317  ennnfonelemom  13350  ennnfoneleminc  13353  ennnfonelemhf1o  13355  ennnfonelemex  13356  ennnfonelemhom  13357  ennnfonelemdm  13362  ennnfonelemr  13365  ennnfonelemim  13366  exmidunben  13368  ctinfom  13370  inffinp1  13371  ctinf  13372  enctlem  13374  ctiunctlemu1st  13376  ctiunctlemu2nd  13377  ctiunctlemudc  13379  ctiunct  13382  ctiunctal  13383  unct  13384  ssomct  13387  nninfdclemcl  13390  nninfdclemp1  13392  nninfdc  13395  structcnvcnv  13419  setscom  13443  relelbasov  13467  ressbas2d  13473  ressval3d  13477  ressabsg  13481  restid2  13653  imasaddfnlemg  13686  quslem  13696  ercpbl  13703  fnpr2ob  13712  mgmplusf  13737  grpinvalem  13756  grpinva  13757  grprida  13758  fngzsum  13759  gzsumvalx  13760  gzsum0  13764  gzsumval2  13765  ismnd  13783  mhmpropd  13824  grppropd  13873  grpsubf  13935  dfgrp3mlem  13954  mulgnn0p1  13987  mulgnn0subcl  13989  mulgsubcl  13990  mulgneg  13994  mulgnn0dir  14006  mulgnn0ass  14012  submmulg  14020  issubg2m  14043  issubg4m  14047  ghmmulg  14110  ghmrn  14111  gsumvalfi  14203  gzsumgsum  14206  gsumf1ofi  14211  gsummhmfi  14215  gsumressfi  14218  lringuplu  14554  rrgsupp  14625  opprdrng  14671  lmodscaf  14698  lssintclm  14772  lspun0  14813  lidlbas  14866  psrbagconcl  15115  psr1clfi  15131  topontopon  15173  eltg3i  15209  epttop  15243  difopn  15261  uncld  15266  0nnei  15306  resttopon  15324  restabs  15328  restopnb  15334  lmcvg  15370  cnptopco  15375  cnss1  15379  cnss2  15380  cncnpi  15381  cncnp2m  15384  cnrest  15388  cnrest2  15389  cnrest2r  15390  cnptoprest  15392  cnptoprest2  15393  lmss  15399  lmff  15402  lmtopcnp  15403  lmcn  15404  txbasval  15420  upxp  15425  txcnmpt  15426  txdis1cn  15431  txlm  15432  lmcn2  15433  cnmpt11  15436  cnmpt11f  15437  cnmpt1t  15438  cnmpt12  15440  cnmpt21  15444  cnmpt21f  15445  cnmpt2t  15446  cnmpt22  15447  cnmpt22f  15448  cnmptcom  15451  hmeocnv  15460  hmeof1o  15462  hmeores  15468  txhmeo  15472  txswaphmeo  15474  isxmet2d  15501  blfvalps  15538  xblss2ps  15557  xblss2  15558  blfps  15562  blf  15563  unirnblps  15575  unirnbl  15576  isxms2  15605  bdxmet  15654  bdmet  15655  xmetxp  15660  xmettx  15663  blssioo  15706  tgioo  15707  mulcncflem  15760  divcncfap  15767  dedekindeulemuub  15770  dedekindeulemub  15771  dedekindeulemloc  15772  dedekindeulemlu  15774  suplociccreex  15777  suplociccex  15778  dedekindicclemuub  15779  dedekindicclemub  15780  dedekindicclemloc  15781  dedekindicclemlu  15783  dedekindicc  15786  ivthinclemlopn  15789  ivthinclemuopn  15791  ivthdich  15806  limcrcl  15811  limcmpted  15816  limccnp2lem  15829  limccnp2cntop  15830  limccoap  15831  dvrecap  15866  plyaddlem1  15900  plymullem1  15901  plycoeid3  15910  plyco  15912  plycj  15914  plyrecj  15916  dvply1  15918  dvply2g  15919  cosordlem  16003  logbgcd1irraplemexp  16126  logbgcd1irrap  16128  zprmlogbaplem2  16138  zprmlogbaplem3  16139  birthdaylem2  16148  birthdaylem3  16149  chtqge0  16169  ppiprm  16181  ppinprm  16182  chtprm  16183  chtnprm  16184  chtqwordi  16185  ppiqltx  16203  bposlem2  16234  lgsneg1  16266  lgsdilem  16268  lgsdir2  16274  lgsdirprm  16275  lgsdir  16276  lgsne0  16279  lgsabs1  16280  lgsdirnn0  16288  lgsdinn0  16289  gausslemma2dlem1f1o  16301  gausslemma2dlem4  16305  lgseisenlem1  16311  lgsquadlem3  16320  2lgslem1a  16329  2sqlem5  16360  2sqlem7  16362  2sqlem8a  16363  2sqlem8  16364  2sqlem9  16365  gropeld  16412  grstructeld2dom  16413  uhgrm  16441  upgrm  16463  upgr1een  16487  uhgredgm  16499  edgupgren  16504  edgumgren  16505  edgusgren  16526  ausgrusgrben  16531  umgr2edg1  16572  usgredg2vlem1  16585  uhgr0enedgfi  16599  subupgr  16636  vtxedgfi  16652  vtxlpfi  16653  vtxdumgrfival  16661  vtxd0nedgbfi  16662  1hevtxdg0fi  16670  p1evtxdeqfilem  16674  wlkvtxm  16703  g0wlk0  16733  wlkres  16742  trlreslem  16752  clwwlkccatlem  16763  clwwlknnn  16775  trlsegvdeglem6  16828  eupth2lem3lem3fi  16833  eupth2lem3lem7fi  16837  eulerpathum  16844  dichmul0or  16882  bj-stand  16898  bj-charfundcALT  16957  bj-charfunbi  16959  bj-bdfindis  17095  bj-peano4  17103  strcollnfALT  17134  pw1map  17147  pwtrufal  17149  pwf1oexmid  17151  subctctexmid  17152  pw1nct  17155  stnot  17161  wexmiddc  17164  nnsf  17170  nninfalllem1  17173  nninfall  17174  nninfsellemqall  17180  nnnninfen  17186  exmidsbthrlem  17189  sbthom  17193  repiecef  17199  cvgcmp2nlemabs  17203  trilpo  17214  iswomni0  17223  redcwlpo  17227  dceqnconst  17232  dcapnconst  17233  nconstwlpolem  17237  nconstwlpo  17238  neapmkvlem  17239  neapmkv  17240  ltlenmkv  17242  taupi  17245  als1d  17255  als2d  17256  rals1d  17257  rals2d  17258  alseu1d  17291  alseu2d  17292  ralseu1d  17293  ralseu2d  17294  dfalseu2  17299