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  isores1  6013  riota2df  6053  acexmidlemcase  6073  brabvv  6127  funoprabg  6180  fnovim  6190  ovmpodf  6213  ovi3  6219  elmpocl  6277  uchoice  6364  1stcof  6390  2ndcof  6391  opabn1stprc  6422  fnmpo  6431  fmpoco  6445  fo2ndf  6456  f1o2ndf1  6457  disjxp1  6465  fvdifsuppst  6477  fsuppeq  6480  fsuppeqg  6481  suppssrst  6494  suppssrgst  6495  brtpos2  6515  reldmtpos  6517  dftpos3  6526  dftpos4  6527  tpostpos2  6529  tposf2  6532  tposf12  6533  tposfo  6535  tposf  6536  smores2  6558  tfrlem1  6572  tfrlem3-2d  6576  tfrlemisucaccv  6589  tfrlemibxssdm  6591  tfrlemibfn  6592  tfrlemi1  6596  tfrexlem  6598  tfr1onlemsucaccv  6605  tfr1onlembxssdm  6607  tfr1onlembfn  6608  tfr1onlemaccex  6612  tfrcllemsucaccv  6618  tfrcllembxssdm  6620  tfrcllembfn  6621  tfrcllemaccex  6625  tfrcldm  6627  rdgivallem  6645  rdgisucinc  6649  frecabex  6662  frecfnom  6665  frecfcllem  6668  frecsuclem  6670  omsuc  6738  nntri2  6760  nnsucuniel  6761  nnsseleq  6767  nnm00  6796  ecexr  6805  swoer  6828  elqsn0m  6870  iinerm  6874  erinxp  6876  ecinxp  6877  eroveu  6893  eroprf  6895  mapprc  6919  mapsn  6965  ixpprc  6994  ixp0  7006  resixp  7008  elixpsn  7010  dom2lem  7051  fundmen  7087  1dom1el  7100  dom0  7131  xpf1o  7137  mapxpen  7141  xpmapenlem  7142  ssenen  7145  nneneq  7151  ssfilem  7170  ssfilemd  7172  dif1en  7176  dif1enen  7177  fin0  7182  fin0or  7183  diffitest  7184  diffisn  7190  ac6sfi  7195  fimax2gtrilemstep  7198  fimax2gtri  7199  finexdc  7200  eqsndc  7203  exmidpweq  7209  pw1fin  7210  onunsnss  7217  unsnfidcel  7221  undifdcss  7223  undifdc  7224  tpfidceq  7230  fiintim  7231  fisseneq  7235  fidcenumlemr  7265  sbthlemi4  7270  sbthlemi5  7271  sbthlemi9  7275  fifo  7307  2omap  7311  suplubti  7333  supelti  7335  infmoti  7361  infisoti  7365  djulclb  7388  updjud  7415  omp1eomlem  7427  0ct  7440  ctmlemr  7441  ctssdclemn0  7443  ctssdccl  7444  ctssdc  7446  enumct  7448  nninfninc  7456  nnnninfeq2  7462  finomni  7473  fodjuomnilemdc  7477  fodjum  7479  fodjuomnilemres  7481  fodjumkvlemres  7492  omniwomnimkv  7500  nninfwlporlem  7506  nninfwlpoimlemginf  7509  nninfwlpoim  7512  nninfinfwlpo  7513  ficardon  7527  pr2cv1  7534  exmidonfinlem  7538  en2eleq  7540  exmidfodomrlemeldju  7544  exmidfodomrlemreseldju  7545  exmidfodomrlemim  7546  finacn  7553  acfun  7556  exmidaclem  7557  exmidontriimlem3  7572  exmidontriimlem4  7573  exmidontriim  7574  pw1if  7577  pw1on  7578  papsym  7605  papcotr  7606  dftap2  7610  2omotaplemst  7617  exmidapne  7619  ccfunen  7623  cc1  7624  cc2lem  7625  cc2  7626  cc3  7627  acnccim  7631  elni2  7674  indpi  7702  distrnqg  7747  subhalfnqq  7774  enq0sym  7792  enq0ref  7793  enq0tr  7794  nqnq0pi  7798  nnnq0lem1  7806  distrnq0  7819  elinp  7834  elnp1st2nd  7836  prltlu  7847  prnmaxl  7848  prnminu  7849  prarloc  7863  nqprm  7902  appdivnq  7923  prmuloc  7926  mullocpr  7931  distrlem4prl  7944  distrlem4pru  7945  ltexprlemm  7960  ltexprlemopl  7961  ltexprlemopu  7963  cauappcvgprlemopl  8006  cauappcvgprlemopu  8008  cauappcvgprlemdisj  8011  cauappcvgprlem2  8020  cauappcvgprlemlim  8021  caucvgprlemnkj  8026  caucvgprlemopl  8029  caucvgprlemopu  8031  caucvgprlemdisj  8034  caucvgprlemcl  8036  caucvgprlemladdfu  8037  caucvgprlemladdrl  8038  caucvgprlem2  8040  caucvgprprlemcbv  8047  caucvgprprlemval  8048  caucvgprprlemlol  8058  caucvgprprlemexbt  8066  caucvgprprlem1  8069  suplocexprlemrl  8077  suplocexprlemmu  8078  suplocexprlemru  8079  suplocexprlemdisj  8080  suplocexprlemloc  8081  suplocexprlemub  8083  suplocexprlemlub  8084  prsrlem1  8102  gt0srpr  8108  caucvgsrlemcl  8149  caucvgsrlembound  8154  caucvgsrlemgt1  8155  suplocsrlemb  8166  suplocsrlem  8168  suplocsr  8169  ltresr  8199  nnindnn  8253  axcaucvglemcl  8255  axcaucvglemval  8257  axcaucvglemcau  8258  axcaucvglemres  8259  axpre-suploclemres  8261  axpre-suploc  8262  sup3exmid  9280  nnind  9302  nn0supp  9601  nn0ge2m1nn  9609  zleloe  9673  zapne  9701  nn0lt2  9709  suprzclex  9726  zindd  9746  uzm1  9935  uzin  9937  infregelbex  9980  elnn1uz2  9989  nn01to3  9999  divfnzn  10003  qapne  10021  xrltnsym2  10178  xaddass  10253  xleadd1a  10257  xlt2add  10264  xlesubadd  10267  iooval2  10299  icoshftf1o  10375  fztri3or  10425  fzneuz  10489  4fvwrd4  10528  elfzo0  10574  infssuzex  10647  infssuzcldc  10649  infssfzcldc  10650  infssfzledc  10651  suprzubdc  10652  nninfdcex  10653  zsupssdc  10654  exbtwnzlemex  10665  ioom  10676  fzfig  10848  uzennn  10854  uzsinds  10862  iseqovex  10876  seq3val  10878  seqvalcd  10879  seqf  10882  seqovcd  10885  monoord2  10904  iseqf1olemjpcl  10926  iseqf1olemqpcl  10927  seq3f1olemqsum  10931  seq3f1o  10935  seqf1og  10939  seq3distr  10950  expp1  10964  expcl2lemap  10969  expclzap  10982  expap0i  10989  nn0ltexp2  11128  bcval5  11182  hashinfuni  11197  hashennnuni  11199  hashnncl  11215  resunimafz0  11255  hashf1lem2  11267  hashf1  11268  zfz1isolemiso  11272  zfz1isolem1  11273  zfz1iso  11274  wrdsymb0  11318  wrdlen1  11323  ccat1st1st  11390  swrdrlen  11414  pfxid  11439  pfxwrdsymbg  11443  pfxtrcfv  11446  pfxccat1  11455  pfxpfxid  11462  pfxcctswrd  11463  swrdccatin1  11478  pfxccatin12  11486  pfxccatid  11494  seq3shft  11584  cvg1nlemcau  11731  rexanuz  11735  resqrexlemoverl  11768  resqrexlemglsq  11769  resqrexlemsqa  11771  resqrexlemex  11772  rersqreu  11775  caubnd2  11864  maxleast  11960  fimaxre2  11974  minmax  11977  xrmaxiflemcl  11992  xrmaxiflemab  11994  xrmaxiflemlub  11995  xrmaxadd  12008  xrminmax  12012  xrbdtri  12023  climreu  12044  reccn2ap  12060  iserex  12086  climcvg1nlem  12096  serf0  12099  fz1f1o  12122  summodclem3  12128  zsumdc  12132  fsum3  12135  isumz  12137  isumss  12139  isumss2  12141  fsumsersdc  12143  fsum3ser  12145  fsumsplit  12155  isumclim2  12170  isumclim3  12171  fsum2dlemstep  12182  fsumcnv  12185  fisumcom2  12186  bcxmas  12237  isumle  12243  cvgratnnlemnexp  12272  cvgratnnlemmn  12273  cvgratz  12280  mertenslemub  12282  mertenslemi1  12283  mertenslem2  12284  mertensabs  12285  zproddc  12327  prod1dc  12334  fprodsplitdc  12344  fprodsplit  12345  fprodunsn  12352  fprodcl2lem  12353  fprodcllemf  12361  fprod2dlemstep  12370  fprodcnv  12373  fprodcom2fi  12374  fprodle  12388  ef0lem  12408  fsumdvds  12590  mod2eq1n2dvds  12627  ndvdssub  12678  bitsfzolem  12702  bitsfzo  12703  bitsinv1  12710  gcdsupex  12715  gcdsupcl  12716  bezoutlemnewy  12754  bezoutlemmain  12756  bezoutlembi  12763  bezoutlemeu  12765  bezoutlemle  12766  uzwodc  12795  nnwofdc  12796  nnwosdc  12797  nninfctlemfo  12798  nninfct  12799  nn0seqcvgd  12800  eucalgf  12814  eucalginv  12815  lcmval  12822  prmind2  12879  dfphi2  12979  phiprmpw  12981  phimullem  12984  eulerthlem1  12986  eulerthlemrprm  12988  eulerthlema  12989  eulerthlemh  12990  eulerthlemth  12991  eulerth  12992  phisum  13000  odzcllem  13002  odzdvds  13005  pythagtriplem19  13042  pclemub  13047  pcprecl  13049  pceu  13055  pcqmul  13063  pcqcl  13066  pcxnn0cl  13070  pcxqcl  13072  pcge0  13073  pcdvdsb  13080  pceq0  13082  pcneg  13085  pcdvdstr  13087  pcgcd1  13088  pc2dvds  13090  pcz  13092  pcprmpw2  13093  pcaddlem  13099  pcadd  13100  pcmptcl  13102  pcmpt  13103  pcmptdvds  13105  fldivp1  13108  qexpz  13112  pockthlem  13116  pockthg  13117  prmunb  13122  1arith  13127  4sqlemffi  13156  4sqlem17  13167  4sqlem18  13168  4sqlem19  13169  ballotfilemcdc  13204  ballotfilem2  13209  ballotfilemfp1  13212  ballotfilemfc0  13213  ballotfilemfcc  13214  ballotfilemfmpn  13215  ballotfilemefi  13218  ballotfilemiex  13225  ballotfilemro  13247  ennnfonelemom  13280  ennnfoneleminc  13283  ennnfonelemhf1o  13285  ennnfonelemex  13286  ennnfonelemhom  13287  ennnfonelemdm  13292  ennnfonelemr  13295  ennnfonelemim  13296  exmidunben  13298  ctinfom  13300  inffinp1  13301  ctinf  13302  enctlem  13304  ctiunctlemu1st  13306  ctiunctlemu2nd  13307  ctiunctlemudc  13309  ctiunct  13312  ctiunctal  13313  unct  13314  ssomct  13317  nninfdclemcl  13320  nninfdclemp1  13322  nninfdc  13325  structcnvcnv  13349  setscom  13373  relelbasov  13396  ressbas2d  13402  ressval3d  13406  ressabsg  13410  restid2  13582  imasaddfnlemg  13615  quslem  13625  ercpbl  13632  fnpr2ob  13641  mgmplusf  13666  grpinvalem  13685  grpinva  13686  grprida  13687  fngzsum  13688  gzsumvalx  13689  gzsum0  13693  gzsumval2  13694  ismnd  13712  mhmpropd  13753  grppropd  13802  grpsubf  13864  dfgrp3mlem  13883  mulgnn0p1  13916  mulgnn0subcl  13918  mulgsubcl  13919  mulgneg  13923  mulgnn0dir  13935  mulgnn0ass  13941  submmulg  13949  issubg2m  13972  issubg4m  13976  ghmmulg  14039  ghmrn  14040  gsumvalfi  14132  gzsumgsum  14135  gsumf1ofi  14140  gsummhmfi  14144  gsumressfi  14147  lringuplu  14479  rrgsupp  14550  opprdrng  14596  lmodscaf  14622  lssintclm  14696  lspun0  14737  lidlbas  14790  psrbagconcl  14989  psr1clfi  15005  topontopon  15047  eltg3i  15083  epttop  15117  difopn  15135  uncld  15140  0nnei  15180  resttopon  15198  restabs  15202  restopnb  15208  lmcvg  15244  cnptopco  15249  cnss1  15253  cnss2  15254  cncnpi  15255  cncnp2m  15258  cnrest  15262  cnrest2  15263  cnrest2r  15264  cnptoprest  15266  cnptoprest2  15267  lmss  15273  lmff  15276  lmtopcnp  15277  lmcn  15278  txbasval  15294  upxp  15299  txcnmpt  15300  txdis1cn  15305  txlm  15306  lmcn2  15307  cnmpt11  15310  cnmpt11f  15311  cnmpt1t  15312  cnmpt12  15314  cnmpt21  15318  cnmpt21f  15319  cnmpt2t  15320  cnmpt22  15321  cnmpt22f  15322  cnmptcom  15325  hmeocnv  15334  hmeof1o  15336  hmeores  15342  txhmeo  15346  txswaphmeo  15348  isxmet2d  15375  blfvalps  15412  xblss2ps  15431  xblss2  15432  blfps  15436  blf  15437  unirnblps  15449  unirnbl  15450  isxms2  15479  bdxmet  15528  bdmet  15529  xmetxp  15534  xmettx  15537  blssioo  15580  tgioo  15581  mulcncflem  15634  divcncfap  15641  dedekindeulemuub  15644  dedekindeulemub  15645  dedekindeulemloc  15646  dedekindeulemlu  15648  suplociccreex  15651  suplociccex  15652  dedekindicclemuub  15653  dedekindicclemub  15654  dedekindicclemloc  15655  dedekindicclemlu  15657  dedekindicc  15660  ivthinclemlopn  15663  ivthinclemuopn  15665  ivthdich  15680  limcrcl  15685  limcmpted  15690  limccnp2lem  15703  limccnp2cntop  15704  limccoap  15705  dvrecap  15740  plyaddlem1  15774  plymullem1  15775  plycoeid3  15784  plyco  15786  plycj  15788  plyrecj  15790  dvply1  15792  dvply2g  15793  cosordlem  15876  logbgcd1irraplemexp  15996  logbgcd1irrap  15998  lgsneg1  16061  lgsdilem  16063  lgsdir2  16069  lgsdirprm  16070  lgsdir  16071  lgsne0  16074  lgsabs1  16075  lgsdirnn0  16083  lgsdinn0  16084  gausslemma2dlem1f1o  16096  gausslemma2dlem4  16100  lgseisenlem1  16106  lgsquadlem3  16115  2lgslem1a  16124  2sqlem5  16155  2sqlem7  16157  2sqlem8a  16158  2sqlem8  16159  2sqlem9  16160  gropeld  16207  grstructeld2dom  16208  uhgrm  16236  upgrm  16258  upgr1een  16282  uhgredgm  16294  edgupgren  16299  edgumgren  16300  edgusgren  16321  ausgrusgrben  16326  umgr2edg1  16367  usgredg2vlem1  16380  uhgr0enedgfi  16394  subupgr  16431  vtxedgfi  16447  vtxlpfi  16448  vtxdumgrfival  16456  vtxd0nedgbfi  16457  1hevtxdg0fi  16465  p1evtxdeqfilem  16469  wlkvtxm  16498  g0wlk0  16528  wlkres  16537  trlreslem  16547  clwwlkccatlem  16558  clwwlknnn  16570  trlsegvdeglem6  16623  eupth2lem3lem3fi  16628  eupth2lem3lem7fi  16632  eulerpathum  16639  dichmul0or  16677  bj-stand  16693  bj-charfundcALT  16752  bj-charfunbi  16754  bj-bdfindis  16890  bj-peano4  16898  strcollnfALT  16929  pw1map  16942  pwtrufal  16944  pwf1oexmid  16946  subctctexmid  16947  pw1nct  16950  nnsf  16956  nninfalllem1  16959  nninfall  16960  nninfsellemqall  16966  nnnninfen  16972  exmidsbthrlem  16975  sbthom  16979  repiecef  16985  cvgcmp2nlemabs  16989  trilpo  17000  iswomni0  17009  redcwlpo  17013  dceqnconst  17018  dcapnconst  17019  nconstwlpolem  17023  nconstwlpo  17024  neapmkvlem  17025  neapmkv  17026  ltlenmkv  17028  taupi  17031  als1d  17041  als2d  17042  rals1d  17043  rals2d  17044