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  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  3772  difprsn1  3852  diftpsn3  3854  difsnss  3859  sneqr  3883  preqr1  3891  preq12b  3893  oprcl  3926  intab  3997  riinm  4083  rintm  4103  disjiun  4123  sndisj  4124  3brtr3g  4161  trint  4242  iinexgm  4288  exmidexmid  4331  exmid01  4333  pwntru  4334  exmid1stab  4343  pwel  4356  exss  4365  0nelop  4386  euotd  4393  opelopabsb  4400  pwunim  4429  issod  4462  frind  4495  suctr  4564  orduniss  4568  onelini  4573  oneluni  4574  eusv2i  4599  rexxfrd  4607  rabxfrd  4613  reuhypd  4615  iunpw  4624  sucexg  4643  ordsucim  4645  ordtriexmidlem  4664  ontriexmidim  4667  ordtri2or2exmidlem  4671  onsucelsucexmidlem  4674  ordsucunielexmid  4676  orddif  4692  suc11g  4702  onintexmid  4718  reg3exmidlemwe  4724  tfisi  4732  peano1  4739  peano2  4740  finds2  4746  omsinds  4767  brrelex12  4811  brel  4825  ssrel  4861  ssrel2  4863  ssrelrel  4873  elrel  4875  xpsspw  4885  relop  4928  dmxpm  5000  opelresi  5072  mptimass  5137  ndmima  5162  poirr2  5178  xpmlem  5206  xpimasn  5234  iotass  5353  iotacl  5360  dffun5r  5387  funeu  5400  funeu2  5401  funfnd  5406  funopg  5409  funun  5420  fununfun  5422  funinsn  5428  funtp  5432  funcnvuni  5448  funcnvres2  5454  imadiflem  5458  imadif  5459  funimaexglem  5462  fneu2  5486  fnimaeq0  5503  fnmpt  5508  ffrn  5543  fun2  5560  f00  5582  f0bi  5583  fimadmfo  5622  foimacnv  5655  resdif  5659  f1ococnv1  5666  fv3  5716  relelfvdm  5725  elfvm  5726  nfvres  5729  dffn5im  5745  mptfvex  5788  fvmptdf  5790  fvmptdv2  5792  fndmdif  5808  dff4im  5848  fmpt  5852  fmptd  5856  fmptdf  5859  f1oresrab  5867  fcoconst  5873  fsn  5874  funopsn  5885  ftpg  5893  fsnunf  5909  resfunexg  5930  mptmex  5939  isores1  6014  riota2df  6054  acexmidlemcase  6074  brabvv  6128  funoprabg  6181  fnovim  6191  ovmpodf  6214  ovi3  6220  elmpocl  6278  uchoice  6365  1stcof  6391  2ndcof  6392  opabn1stprc  6423  fnmpo  6432  fmpoco  6446  fo2ndf  6457  f1o2ndf1  6458  disjxp1  6466  fvdifsuppst  6478  fsuppeq  6481  fsuppeqg  6482  suppssrst  6495  suppssrgst  6496  brtpos2  6516  reldmtpos  6518  dftpos3  6527  dftpos4  6528  tpostpos2  6530  tposf2  6533  tposf12  6534  tposfo  6536  tposf  6537  smores2  6559  tfrlem1  6573  tfrlem3-2d  6577  tfrlemisucaccv  6590  tfrlemibxssdm  6592  tfrlemibfn  6593  tfrlemi1  6597  tfrexlem  6599  tfr1onlemsucaccv  6606  tfr1onlembxssdm  6608  tfr1onlembfn  6609  tfr1onlemaccex  6613  tfrcllemsucaccv  6619  tfrcllembxssdm  6621  tfrcllembfn  6622  tfrcllemaccex  6626  tfrcldm  6628  rdgivallem  6646  rdgisucinc  6650  frecabex  6663  frecfnom  6666  frecfcllem  6669  frecsuclem  6671  omsuc  6739  nntri2  6761  nnsucuniel  6762  nnsseleq  6768  nnm00  6797  ecexr  6806  swoer  6829  elqsn0m  6871  iinerm  6875  erinxp  6877  ecinxp  6878  eroveu  6894  eroprf  6896  mapprc  6920  mapsn  6966  ixpprc  6995  ixp0  7007  resixp  7009  elixpsn  7011  dom2lem  7052  fundmen  7088  1dom1el  7101  dom0  7132  xpf1o  7138  mapxpen  7142  xpmapenlem  7143  ssenen  7146  nneneq  7152  ssfilem  7171  ssfilemd  7173  dif1en  7177  dif1enen  7178  fin0  7183  fin0or  7184  diffitest  7185  diffisn  7191  ac6sfi  7196  fimax2gtrilemstep  7199  fimax2gtri  7200  finexdc  7201  eqsndc  7204  exmidpweq  7210  pw1fin  7211  onunsnss  7218  unsnfidcel  7222  undifdcss  7224  undifdc  7225  tpfidceq  7231  fiintim  7232  fisseneq  7236  fidcenumlemr  7266  sbthlemi4  7271  sbthlemi5  7272  sbthlemi9  7276  fifo  7308  2omap  7312  suplubti  7334  supelti  7336  infmoti  7362  infisoti  7366  djulclb  7389  updjud  7416  omp1eomlem  7428  0ct  7441  ctmlemr  7442  ctssdclemn0  7444  ctssdccl  7445  ctssdc  7447  enumct  7449  nninfninc  7457  nnnninfeq2  7463  finomni  7474  fodjuomnilemdc  7478  fodjum  7480  fodjuomnilemres  7482  fodjumkvlemres  7493  omniwomnimkv  7501  nninfwlporlem  7507  nninfwlpoimlemginf  7510  nninfwlpoim  7513  nninfinfwlpo  7514  ficardon  7528  pr2cv1  7535  exmidonfinlem  7539  en2eleq  7541  exmidfodomrlemeldju  7545  exmidfodomrlemreseldju  7546  exmidfodomrlemim  7547  finacn  7554  acfun  7557  exmidaclem  7558  exmidontriimlem3  7573  exmidontriimlem4  7574  exmidontriim  7575  pw1if  7578  pw1on  7579  papsym  7606  papcotr  7607  dftap2  7611  2omotaplemst  7618  exmidapne  7620  ccfunen  7624  cc1  7625  cc2lem  7626  cc2  7627  cc3  7628  acnccim  7632  elni2  7675  indpi  7703  distrnqg  7748  subhalfnqq  7775  enq0sym  7793  enq0ref  7794  enq0tr  7795  nqnq0pi  7799  nnnq0lem1  7807  distrnq0  7820  elinp  7835  elnp1st2nd  7837  prltlu  7848  prnmaxl  7849  prnminu  7850  prarloc  7864  nqprm  7903  appdivnq  7924  prmuloc  7927  mullocpr  7932  distrlem4prl  7945  distrlem4pru  7946  ltexprlemm  7961  ltexprlemopl  7962  ltexprlemopu  7964  cauappcvgprlemopl  8007  cauappcvgprlemopu  8009  cauappcvgprlemdisj  8012  cauappcvgprlem2  8021  cauappcvgprlemlim  8022  caucvgprlemnkj  8027  caucvgprlemopl  8030  caucvgprlemopu  8032  caucvgprlemdisj  8035  caucvgprlemcl  8037  caucvgprlemladdfu  8038  caucvgprlemladdrl  8039  caucvgprlem2  8041  caucvgprprlemcbv  8048  caucvgprprlemval  8049  caucvgprprlemlol  8059  caucvgprprlemexbt  8067  caucvgprprlem1  8070  suplocexprlemrl  8078  suplocexprlemmu  8079  suplocexprlemru  8080  suplocexprlemdisj  8081  suplocexprlemloc  8082  suplocexprlemub  8084  suplocexprlemlub  8085  prsrlem1  8103  gt0srpr  8109  caucvgsrlemcl  8150  caucvgsrlembound  8155  caucvgsrlemgt1  8156  suplocsrlemb  8167  suplocsrlem  8169  suplocsr  8170  ltresr  8200  nnindnn  8254  axcaucvglemcl  8256  axcaucvglemval  8258  axcaucvglemcau  8259  axcaucvglemres  8260  axpre-suploclemres  8262  axpre-suploc  8263  sup3exmid  9281  nnind  9303  nn0supp  9602  nn0ge2m1nn  9610  zleloe  9674  zapne  9702  nn0lt2  9710  suprzclex  9727  zindd  9747  uzm1  9936  uzin  9938  infregelbex  9981  elnn1uz2  9990  nn01to3  10000  divfnzn  10004  qapne  10022  xrltnsym2  10179  xaddass  10254  xleadd1a  10258  xlt2add  10265  xlesubadd  10268  iooval2  10300  icoshftf1o  10376  fztri3or  10426  fzneuz  10491  4fvwrd4  10530  elfzo0  10576  infssuzex  10649  infssuzcldc  10651  infssfzcldc  10652  infssfzledc  10653  suprzubdc  10654  nninfdcex  10655  zsupssdc  10656  exbtwnzlemex  10667  ioom  10678  fzfig  10850  uzennn  10856  uzsinds  10864  iseqovex  10878  seq3val  10880  seqvalcd  10881  seqf  10884  seqovcd  10887  monoord2  10906  iseqf1olemjpcl  10928  iseqf1olemqpcl  10929  seq3f1olemqsum  10933  seq3f1o  10937  seqf1og  10941  seq3distr  10952  expp1  10966  expcl2lemap  10971  expclzap  10984  expap0i  10991  nn0ltexp2  11130  bcval5  11184  hashinfuni  11199  hashennnuni  11201  hashnncl  11217  resunimafz0  11257  hashf1lem2  11269  hashf1  11270  zfz1isolemiso  11274  zfz1isolem1  11275  zfz1iso  11276  wrdsymb0  11320  wrdlen1  11325  ccat1st1st  11392  swrdrlen  11416  pfxid  11441  pfxwrdsymbg  11445  pfxtrcfv  11448  pfxccat1  11457  pfxpfxid  11464  pfxcctswrd  11465  swrdccatin1  11480  pfxccatin12  11488  pfxccatid  11496  seq3shft  11586  cvg1nlemcau  11733  rexanuz  11737  resqrexlemoverl  11770  resqrexlemglsq  11771  resqrexlemsqa  11773  resqrexlemex  11774  rersqreu  11777  caubnd2  11866  maxleast  11962  fimaxre2  11976  minmax  11979  xrmaxiflemcl  11994  xrmaxiflemab  11996  xrmaxiflemlub  11997  xrmaxadd  12010  xrminmax  12014  xrbdtri  12025  climreu  12046  reccn2ap  12062  iserex  12088  climcvg1nlem  12098  serf0  12101  fz1f1o  12124  summodclem3  12130  zsumdc  12134  fsum3  12137  isumz  12139  isumss  12141  isumss2  12143  fsumsersdc  12145  fsum3ser  12147  fsumsplit  12157  isumclim2  12172  isumclim3  12173  fsum2dlemstep  12184  fsumcnv  12187  fisumcom2  12188  bcxmas  12239  isumle  12245  cvgratnnlemnexp  12274  cvgratnnlemmn  12275  cvgratz  12282  mertenslemub  12284  mertenslemi1  12285  mertenslem2  12286  mertensabs  12287  zproddc  12329  prod1dc  12336  fprodsplitdc  12346  fprodsplit  12347  fprodunsn  12354  fprodcl2lem  12355  fprodcllemf  12363  fprod2dlemstep  12372  fprodcnv  12375  fprodcom2fi  12376  fprodle  12390  ef0lem  12410  fsumdvds  12592  mod2eq1n2dvds  12629  ndvdssub  12680  bitsfzolem  12704  bitsfzo  12705  bitsinv1  12712  gcdsupex  12717  gcdsupcl  12718  bezoutlemnewy  12756  bezoutlemmain  12758  bezoutlembi  12765  bezoutlemeu  12767  bezoutlemle  12768  uzwodc  12797  nnwofdc  12798  nnwosdc  12799  nninfctlemfo  12800  nninfct  12801  nn0seqcvgd  12802  eucalgf  12816  eucalginv  12817  lcmval  12824  prmind2  12881  dfphi2  12981  phiprmpw  12983  phimullem  12986  eulerthlem1  12988  eulerthlemrprm  12990  eulerthlema  12991  eulerthlemh  12992  eulerthlemth  12993  eulerth  12994  phisum  13002  odzcllem  13004  odzdvds  13007  pythagtriplem19  13044  pclemub  13049  pcprecl  13051  pceu  13057  pcqmul  13065  pcqcl  13068  pcxnn0cl  13072  pcxqcl  13074  pcge0  13075  pcdvdsb  13082  pceq0  13084  pcneg  13087  pcdvdstr  13089  pcgcd1  13090  pc2dvds  13092  pcz  13094  pcprmpw2  13095  pcaddlem  13101  pcadd  13102  pcmptcl  13104  pcmpt  13105  pcmptdvds  13107  fldivp1  13110  qexpz  13114  pockthlem  13118  pockthg  13119  prmunb  13124  1arith  13129  4sqlemffi  13158  4sqlem17  13169  4sqlem18  13170  4sqlem19  13171  ballotfilemcdc  13206  ballotfilem2  13211  ballotfilemfp1  13214  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemfmpn  13217  ballotfilemefi  13220  ballotfilemiex  13227  ballotfilemro  13249  ennnfonelemom  13282  ennnfoneleminc  13285  ennnfonelemhf1o  13287  ennnfonelemex  13288  ennnfonelemhom  13289  ennnfonelemdm  13294  ennnfonelemr  13297  ennnfonelemim  13298  exmidunben  13300  ctinfom  13302  inffinp1  13303  ctinf  13304  enctlem  13306  ctiunctlemu1st  13308  ctiunctlemu2nd  13309  ctiunctlemudc  13311  ctiunct  13314  ctiunctal  13315  unct  13316  ssomct  13319  nninfdclemcl  13322  nninfdclemp1  13324  nninfdc  13327  structcnvcnv  13351  setscom  13375  relelbasov  13399  ressbas2d  13405  ressval3d  13409  ressabsg  13413  restid2  13585  imasaddfnlemg  13618  quslem  13628  ercpbl  13635  fnpr2ob  13644  mgmplusf  13669  grpinvalem  13688  grpinva  13689  grprida  13690  fngzsum  13691  gzsumvalx  13692  gzsum0  13696  gzsumval2  13697  ismnd  13715  mhmpropd  13756  grppropd  13805  grpsubf  13867  dfgrp3mlem  13886  mulgnn0p1  13919  mulgnn0subcl  13921  mulgsubcl  13922  mulgneg  13926  mulgnn0dir  13938  mulgnn0ass  13944  submmulg  13952  issubg2m  13975  issubg4m  13979  ghmmulg  14042  ghmrn  14043  gsumvalfi  14135  gzsumgsum  14138  gsumf1ofi  14143  gsummhmfi  14147  gsumressfi  14150  lringuplu  14486  rrgsupp  14557  opprdrng  14603  lmodscaf  14630  lssintclm  14704  lspun0  14745  lidlbas  14798  psrbagconcl  15046  psr1clfi  15062  topontopon  15104  eltg3i  15140  epttop  15174  difopn  15192  uncld  15197  0nnei  15237  resttopon  15255  restabs  15259  restopnb  15265  lmcvg  15301  cnptopco  15306  cnss1  15310  cnss2  15311  cncnpi  15312  cncnp2m  15315  cnrest  15319  cnrest2  15320  cnrest2r  15321  cnptoprest  15323  cnptoprest2  15324  lmss  15330  lmff  15333  lmtopcnp  15334  lmcn  15335  txbasval  15351  upxp  15356  txcnmpt  15357  txdis1cn  15362  txlm  15363  lmcn2  15364  cnmpt11  15367  cnmpt11f  15368  cnmpt1t  15369  cnmpt12  15371  cnmpt21  15375  cnmpt21f  15376  cnmpt2t  15377  cnmpt22  15378  cnmpt22f  15379  cnmptcom  15382  hmeocnv  15391  hmeof1o  15393  hmeores  15399  txhmeo  15403  txswaphmeo  15405  isxmet2d  15432  blfvalps  15469  xblss2ps  15488  xblss2  15489  blfps  15493  blf  15494  unirnblps  15506  unirnbl  15507  isxms2  15536  bdxmet  15585  bdmet  15586  xmetxp  15591  xmettx  15594  blssioo  15637  tgioo  15638  mulcncflem  15691  divcncfap  15698  dedekindeulemuub  15701  dedekindeulemub  15702  dedekindeulemloc  15703  dedekindeulemlu  15705  suplociccreex  15708  suplociccex  15709  dedekindicclemuub  15710  dedekindicclemub  15711  dedekindicclemloc  15712  dedekindicclemlu  15714  dedekindicc  15717  ivthinclemlopn  15720  ivthinclemuopn  15722  ivthdich  15737  limcrcl  15742  limcmpted  15747  limccnp2lem  15760  limccnp2cntop  15761  limccoap  15762  dvrecap  15797  plyaddlem1  15831  plymullem1  15832  plycoeid3  15841  plyco  15843  plycj  15845  plyrecj  15847  dvply1  15849  dvply2g  15850  cosordlem  15933  logbgcd1irraplemexp  16053  logbgcd1irrap  16055  birthdaylem2  16071  birthdaylem3  16072  lgsneg1  16127  lgsdilem  16129  lgsdir2  16135  lgsdirprm  16136  lgsdir  16137  lgsne0  16140  lgsabs1  16141  lgsdirnn0  16149  lgsdinn0  16150  gausslemma2dlem1f1o  16162  gausslemma2dlem4  16166  lgseisenlem1  16172  lgsquadlem3  16181  2lgslem1a  16190  2sqlem5  16221  2sqlem7  16223  2sqlem8a  16224  2sqlem8  16225  2sqlem9  16226  gropeld  16273  grstructeld2dom  16274  uhgrm  16302  upgrm  16324  upgr1een  16348  uhgredgm  16360  edgupgren  16365  edgumgren  16366  edgusgren  16387  ausgrusgrben  16392  umgr2edg1  16433  usgredg2vlem1  16446  uhgr0enedgfi  16460  subupgr  16497  vtxedgfi  16513  vtxlpfi  16514  vtxdumgrfival  16522  vtxd0nedgbfi  16523  1hevtxdg0fi  16531  p1evtxdeqfilem  16535  wlkvtxm  16564  g0wlk0  16594  wlkres  16603  trlreslem  16613  clwwlkccatlem  16624  clwwlknnn  16636  trlsegvdeglem6  16689  eupth2lem3lem3fi  16694  eupth2lem3lem7fi  16698  eulerpathum  16705  dichmul0or  16743  bj-stand  16759  bj-charfundcALT  16818  bj-charfunbi  16820  bj-bdfindis  16956  bj-peano4  16964  strcollnfALT  16995  pw1map  17008  pwtrufal  17010  pwf1oexmid  17012  subctctexmid  17013  pw1nct  17016  nnsf  17022  nninfalllem1  17025  nninfall  17026  nninfsellemqall  17032  nnnninfen  17038  exmidsbthrlem  17041  sbthom  17045  repiecef  17051  cvgcmp2nlemabs  17055  trilpo  17066  iswomni0  17075  redcwlpo  17079  dceqnconst  17084  dcapnconst  17085  nconstwlpolem  17089  nconstwlpo  17090  neapmkvlem  17091  neapmkv  17092  ltlenmkv  17094  taupi  17097  als1d  17107  als2d  17108  rals1d  17109  rals2d  17110  alseu1d  17143  alseu2d  17144  ralseu1d  17145  ralseu2d  17146  dfalseu2  17151