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  737  3mix3  1195  mpjao3dan  1344  ecase23d  1387  exlimdh  1645  nexd  1662  alexnim  1697  excomim  1711  19.41  1734  equcomd  1755  nfexd  1810  sbh  1825  sbcof2  1859  sbidm  1900  sb6rf  1902  nfsbt  2032  dvelimALT  2066  dvelimfv  2067  dvelimor  2074  eu2  2127  2euex  2170  eqcomd  2240  3eltr3g  2319  abbid  2351  neneqd  2435  eqnetrrid  2445  3netr3g  2448  necomd  2500  r19.21bi  2632  nrexdv  2637  rexlimd  2659  rabbidva  2803  elisset  2830  euind  3007  rmoan  3020  reuind  3025  2rmorex  3026  spsbc  3057  spesbc  3132  eldifad  3225  eldifbd  3226  3sstr3g  3284  sseqtrdi  3290  difindiss  3479  un00  3559  undifss  3594  ifcldcd  3664  disjpr2  3758  difprsn1  3838  diftpsn3  3840  difsnss  3845  sneqr  3869  preqr1  3877  preq12b  3879  oprcl  3912  intab  3983  riinm  4069  rintm  4089  disjiun  4109  sndisj  4110  3brtr3g  4147  trint  4228  iinexgm  4271  exmidexmid  4314  exmid01  4316  pwntru  4317  exmid1stab  4326  pwel  4339  exss  4348  0nelop  4369  euotd  4376  opelopabsb  4383  pwunim  4412  issod  4445  frind  4478  suctr  4547  orduniss  4551  onelini  4556  oneluni  4557  eusv2i  4581  rexxfrd  4589  rabxfrd  4595  reuhypd  4597  iunpw  4606  sucexg  4625  ordsucim  4627  ordtriexmidlem  4646  ontriexmidim  4649  ordtri2or2exmidlem  4653  onsucelsucexmidlem  4656  ordsucunielexmid  4658  orddif  4674  suc11g  4684  onintexmid  4700  reg3exmidlemwe  4706  tfisi  4714  peano1  4721  peano2  4722  finds2  4728  omsinds  4749  brrelex12  4793  brel  4807  ssrel  4843  ssrel2  4845  ssrelrel  4855  elrel  4857  xpsspw  4867  relop  4910  dmxpm  4982  opelresi  5054  mptimass  5119  ndmima  5144  poirr2  5160  xpmlem  5188  xpimasn  5216  iotass  5335  iotacl  5342  dffun5r  5369  funeu  5382  funeu2  5383  funfnd  5388  funopg  5391  funun  5402  fununfun  5404  funinsn  5410  funtp  5414  funcnvuni  5430  funcnvres2  5436  imadiflem  5440  imadif  5441  funimaexglem  5444  fneu2  5468  fnimaeq0  5485  fnmpt  5490  ffrn  5525  fun2  5542  f00  5564  f0bi  5565  fimadmfo  5604  foimacnv  5637  resdif  5641  f1ococnv1  5648  fv3  5698  relelfvdm  5707  elfvm  5708  nfvres  5711  dffn5im  5727  mptfvex  5768  fvmptdf  5770  fvmptdv2  5772  fndmdif  5788  dff4im  5828  fmpt  5832  fmptd  5836  fmptdf  5839  f1oresrab  5847  fcoconst  5853  fsn  5854  funopsn  5865  ftpg  5873  fsnunf  5889  resfunexg  5910  isores1  5993  riota2df  6033  acexmidlemcase  6053  brabvv  6107  funoprabg  6160  fnovim  6170  ovmpodf  6193  ovi3  6199  elmpocl  6257  uchoice  6344  1stcof  6370  2ndcof  6371  opabn1stprc  6402  fnmpo  6411  fmpoco  6425  fo2ndf  6436  f1o2ndf1  6437  disjxp1  6445  fvdifsuppst  6457  fsuppeq  6460  fsuppeqg  6461  suppssrst  6474  suppssrgst  6475  brtpos2  6495  reldmtpos  6497  dftpos3  6506  dftpos4  6507  tpostpos2  6509  tposf2  6512  tposf12  6513  tposfo  6515  tposf  6516  smores2  6538  tfrlem1  6552  tfrlem3-2d  6556  tfrlemisucaccv  6569  tfrlemibxssdm  6571  tfrlemibfn  6572  tfrlemi1  6576  tfrexlem  6578  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemaccex  6592  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemaccex  6605  tfrcldm  6607  rdgivallem  6625  rdgisucinc  6629  frecabex  6642  frecfnom  6645  frecfcllem  6648  frecsuclem  6650  omsuc  6718  nntri2  6740  nnsucuniel  6741  nnsseleq  6747  nnm00  6776  ecexr  6785  swoer  6808  elqsn0m  6850  iinerm  6854  erinxp  6856  ecinxp  6857  eroveu  6873  eroprf  6875  mapprc  6899  mapsn  6938  ixpprc  6967  ixp0  6979  resixp  6981  elixpsn  6983  dom2lem  7024  fundmen  7060  1dom1el  7073  dom0  7104  xpf1o  7110  mapxpen  7114  xpmapenlem  7115  ssenen  7118  nneneq  7124  ssfilem  7143  ssfilemd  7145  dif1en  7149  dif1enen  7150  fin0  7155  fin0or  7156  diffitest  7157  diffisn  7163  ac6sfi  7168  fimax2gtrilemstep  7171  fimax2gtri  7172  finexdc  7173  eqsndc  7176  exmidpweq  7182  pw1fin  7183  onunsnss  7190  unsnfidcel  7194  undifdcss  7196  undifdc  7197  tpfidceq  7203  fiintim  7204  fisseneq  7208  fidcenumlemr  7238  sbthlemi4  7243  sbthlemi5  7244  sbthlemi9  7248  fifo  7280  2omap  7282  suplubti  7304  supelti  7306  infmoti  7332  infisoti  7336  djulclb  7359  updjud  7386  omp1eomlem  7398  0ct  7411  ctmlemr  7412  ctssdclemn0  7414  ctssdccl  7415  ctssdc  7417  enumct  7419  nninfninc  7427  nnnninfeq2  7433  finomni  7444  fodjuomnilemdc  7448  fodjum  7450  fodjuomnilemres  7452  fodjumkvlemres  7463  omniwomnimkv  7471  nninfwlporlem  7477  nninfwlpoimlemginf  7480  nninfwlpoim  7483  nninfinfwlpo  7484  ficardon  7498  pr2cv1  7505  exmidonfinlem  7509  en2eleq  7511  exmidfodomrlemeldju  7515  exmidfodomrlemreseldju  7516  exmidfodomrlemim  7517  finacn  7524  acfun  7527  exmidaclem  7528  exmidontriimlem3  7543  exmidontriimlem4  7544  exmidontriim  7545  pw1if  7548  pw1on  7549  papsym  7576  papcotr  7577  dftap2  7581  2omotaplemst  7588  exmidapne  7590  ccfunen  7594  cc1  7595  cc2lem  7596  cc2  7597  cc3  7598  acnccim  7602  elni2  7645  indpi  7673  distrnqg  7718  subhalfnqq  7745  enq0sym  7763  enq0ref  7764  enq0tr  7765  nqnq0pi  7769  nnnq0lem1  7777  distrnq0  7790  elinp  7805  elnp1st2nd  7807  prltlu  7818  prnmaxl  7819  prnminu  7820  prarloc  7834  nqprm  7873  appdivnq  7894  prmuloc  7897  mullocpr  7902  distrlem4prl  7915  distrlem4pru  7916  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemopu  7934  cauappcvgprlemopl  7977  cauappcvgprlemopu  7979  cauappcvgprlemdisj  7982  cauappcvgprlem2  7991  cauappcvgprlemlim  7992  caucvgprlemnkj  7997  caucvgprlemopl  8000  caucvgprlemopu  8002  caucvgprlemdisj  8005  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem2  8011  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemlol  8029  caucvgprprlemexbt  8037  caucvgprprlem1  8040  suplocexprlemrl  8048  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  suplocexprlemlub  8055  prsrlem1  8073  gt0srpr  8079  caucvgsrlemcl  8120  caucvgsrlembound  8125  caucvgsrlemgt1  8126  suplocsrlemb  8137  suplocsrlem  8139  suplocsr  8140  ltresr  8170  nnindnn  8224  axcaucvglemcl  8226  axcaucvglemval  8228  axcaucvglemcau  8229  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  sup3exmid  9248  nnind  9270  nn0supp  9569  nn0ge2m1nn  9577  zleloe  9641  zapne  9669  nn0lt2  9677  suprzclex  9694  zindd  9714  uzm1  9903  uzin  9905  infregelbex  9948  elnn1uz2  9957  nn01to3  9967  divfnzn  9971  qapne  9989  xrltnsym2  10146  xaddass  10221  xleadd1a  10225  xlt2add  10232  xlesubadd  10235  iooval2  10267  icoshftf1o  10343  fztri3or  10393  fzneuz  10457  4fvwrd4  10496  elfzo0  10542  infssuzex  10615  infssuzcldc  10617  infssfzcldc  10618  infssfzledc  10619  suprzubdc  10620  nninfdcex  10621  zsupssdc  10622  exbtwnzlemex  10633  ioom  10644  fzfig  10816  uzennn  10822  uzsinds  10830  iseqovex  10844  seq3val  10846  seqvalcd  10847  seqf  10850  seqovcd  10853  monoord2  10872  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  seq3f1olemqsum  10899  seq3f1o  10903  seqf1og  10907  seq3distr  10918  expp1  10932  expcl2lemap  10937  expclzap  10950  expap0i  10957  nn0ltexp2  11096  bcval5  11150  hashinfuni  11165  hashennnuni  11167  hashnncl  11183  resunimafz0  11223  zfz1isolemiso  11236  zfz1isolem1  11237  zfz1iso  11238  wrdsymb0  11282  wrdlen1  11287  ccat1st1st  11354  swrdrlen  11378  pfxid  11403  pfxwrdsymbg  11407  pfxtrcfv  11410  pfxccat1  11419  pfxpfxid  11426  pfxcctswrd  11427  swrdccatin1  11442  pfxccatin12  11450  pfxccatid  11458  seq3shft  11548  cvg1nlemcau  11694  rexanuz  11698  resqrexlemoverl  11731  resqrexlemglsq  11732  resqrexlemsqa  11734  resqrexlemex  11735  rersqreu  11738  caubnd2  11827  maxleast  11923  fimaxre2  11937  minmax  11940  xrmaxiflemcl  11955  xrmaxiflemab  11957  xrmaxiflemlub  11958  xrmaxadd  11971  xrminmax  11975  xrbdtri  11986  climreu  12007  reccn2ap  12023  iserex  12049  climcvg1nlem  12059  serf0  12062  fz1f1o  12085  summodclem3  12091  zsumdc  12095  fsum3  12098  isumz  12100  isumss  12102  isumss2  12104  fsumsersdc  12106  fsum3ser  12108  fsumsplit  12118  isumclim2  12133  isumclim3  12134  fsum2dlemstep  12145  fsumcnv  12148  fisumcom2  12149  bcxmas  12200  isumle  12206  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratz  12243  mertenslemub  12245  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  zproddc  12290  prod1dc  12297  fprodsplitdc  12307  fprodsplit  12308  fprodunsn  12315  fprodcl2lem  12316  fprodcllemf  12324  fprod2dlemstep  12333  fprodcnv  12336  fprodcom2fi  12337  fprodle  12351  ef0lem  12371  fsumdvds  12553  mod2eq1n2dvds  12590  ndvdssub  12641  bitsfzolem  12665  bitsfzo  12666  bitsinv1  12673  gcdsupex  12678  gcdsupcl  12679  bezoutlemnewy  12717  bezoutlemmain  12719  bezoutlembi  12726  bezoutlemeu  12728  bezoutlemle  12729  uzwodc  12758  nnwofdc  12759  nnwosdc  12760  nninfctlemfo  12761  nninfct  12762  nn0seqcvgd  12763  eucalgf  12777  eucalginv  12778  lcmval  12785  prmind2  12842  dfphi2  12942  phiprmpw  12944  phimullem  12947  eulerthlem1  12949  eulerthlemrprm  12951  eulerthlema  12952  eulerthlemh  12953  eulerthlemth  12954  eulerth  12955  phisum  12963  odzcllem  12965  odzdvds  12968  pythagtriplem19  13005  pclemub  13010  pcprecl  13012  pceu  13018  pcqmul  13026  pcqcl  13029  pcxnn0cl  13033  pcxqcl  13035  pcge0  13036  pcdvdsb  13043  pceq0  13045  pcneg  13048  pcdvdstr  13050  pcgcd1  13051  pc2dvds  13053  pcz  13055  pcprmpw2  13056  pcaddlem  13062  pcadd  13063  pcmptcl  13065  pcmpt  13066  pcmptdvds  13068  fldivp1  13071  qexpz  13075  pockthlem  13079  pockthg  13080  prmunb  13085  1arith  13090  4sqlemffi  13119  4sqlem17  13130  4sqlem18  13131  4sqlem19  13132  ballotfilemcdc  13167  ballotfilem2  13172  ballotfilemfp1  13175  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfmpn  13178  ballotfilemefi  13181  ballotfilemiex  13188  ballotfilemro  13210  ennnfonelemom  13243  ennnfoneleminc  13246  ennnfonelemhf1o  13248  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemdm  13255  ennnfonelemr  13258  ennnfonelemim  13259  exmidunben  13261  ctinfom  13263  inffinp1  13264  ctinf  13265  enctlem  13267  ctiunctlemu1st  13269  ctiunctlemu2nd  13270  ctiunctlemudc  13272  ctiunct  13275  ctiunctal  13276  unct  13277  ssomct  13280  nninfdclemcl  13283  nninfdclemp1  13285  nninfdc  13288  structcnvcnv  13312  setscom  13336  relelbasov  13359  ressbas2d  13365  ressval3d  13369  ressabsg  13373  restid2  13545  imasaddfnlemg  13611  quslem  13621  ercpbl  13628  fnpr2ob  13637  mgmplusf  13663  grpinvalem  13682  grpinva  13683  grprida  13684  fngsum  13685  igsumvalx  13686  gsum0g  13693  gsumval2  13694  ismnd  13716  mhmpropd  13763  grppropd  13814  grpsubf  13876  dfgrp3mlem  13895  mulgnn0p1  13934  mulgnn0subcl  13936  mulgsubcl  13937  mulgneg  13941  mulgnn0dir  13953  mulgnn0ass  13959  submmulg  13967  issubg2m  13990  issubg4m  13994  ghmmulg  14057  ghmrn  14058  lringuplu  14426  rrgsupp  14497  opprdrng  14543  lmodscaf  14570  lssintclm  14644  lspun0  14685  lidlbas  14738  psrbagconcl  14939  psr1clfi  14955  topontopon  14997  eltg3i  15033  epttop  15067  difopn  15085  uncld  15090  0nnei  15130  resttopon  15148  restabs  15152  restopnb  15158  lmcvg  15194  cnptopco  15199  cnss1  15203  cnss2  15204  cncnpi  15205  cncnp2m  15208  cnrest  15212  cnrest2  15213  cnrest2r  15214  cnptoprest  15216  cnptoprest2  15217  lmss  15223  lmff  15226  lmtopcnp  15227  lmcn  15228  txbasval  15244  upxp  15249  txcnmpt  15250  txdis1cn  15255  txlm  15256  lmcn2  15257  cnmpt11  15260  cnmpt11f  15261  cnmpt1t  15262  cnmpt12  15264  cnmpt21  15268  cnmpt21f  15269  cnmpt2t  15270  cnmpt22  15271  cnmpt22f  15272  cnmptcom  15275  hmeocnv  15284  hmeof1o  15286  hmeores  15292  txhmeo  15296  txswaphmeo  15298  isxmet2d  15325  blfvalps  15362  xblss2ps  15381  xblss2  15382  blfps  15386  blf  15387  unirnblps  15399  unirnbl  15400  isxms2  15429  bdxmet  15478  bdmet  15479  xmetxp  15484  xmettx  15487  blssioo  15530  tgioo  15531  mulcncflem  15584  divcncfap  15591  dedekindeulemuub  15594  dedekindeulemub  15595  dedekindeulemloc  15596  dedekindeulemlu  15598  suplociccreex  15601  suplociccex  15602  dedekindicclemuub  15603  dedekindicclemub  15604  dedekindicclemloc  15605  dedekindicclemlu  15607  dedekindicc  15610  ivthinclemlopn  15613  ivthinclemuopn  15615  ivthdich  15630  limcrcl  15635  limcmpted  15640  limccnp2lem  15653  limccnp2cntop  15654  limccoap  15655  dvrecap  15690  plyaddlem1  15724  plymullem1  15725  plycoeid3  15734  plyco  15736  plycj  15738  plyrecj  15740  dvply1  15742  dvply2g  15743  cosordlem  15826  logbgcd1irraplemexp  15945  logbgcd1irrap  15947  lgsneg1  16010  lgsdilem  16012  lgsdir2  16018  lgsdirprm  16019  lgsdir  16020  lgsne0  16023  lgsabs1  16024  lgsdirnn0  16032  lgsdinn0  16033  gausslemma2dlem1f1o  16045  gausslemma2dlem4  16049  lgseisenlem1  16055  lgsquadlem3  16064  2lgslem1a  16073  2sqlem5  16104  2sqlem7  16106  2sqlem8a  16107  2sqlem8  16108  2sqlem9  16109  gropeld  16156  grstructeld2dom  16157  uhgrm  16185  upgrm  16207  upgr1een  16231  uhgredgm  16243  edgupgren  16248  edgumgren  16249  edgusgren  16270  ausgrusgrben  16275  umgr2edg1  16316  usgredg2vlem1  16329  uhgr0enedgfi  16343  subupgr  16380  vtxedgfi  16396  vtxlpfi  16397  vtxdumgrfival  16405  vtxd0nedgbfi  16406  1hevtxdg0fi  16414  p1evtxdeqfilem  16418  wlkvtxm  16447  g0wlk0  16477  wlkres  16486  trlreslem  16496  clwwlkccatlem  16507  clwwlknnn  16519  trlsegvdeglem6  16572  eupth2lem3lem3fi  16577  eupth2lem3lem7fi  16581  eulerpathum  16588  bj-stand  16632  bj-charfundcALT  16691  bj-charfunbi  16693  bj-bdfindis  16829  bj-peano4  16837  strcollnfALT  16868  pw1map  16881  pwtrufal  16883  pwf1oexmid  16885  subctctexmid  16886  pw1nct  16889  nnsf  16895  nninfalllem1  16898  nninfall  16899  nninfsellemqall  16905  nnnninfen  16911  exmidsbthrlem  16914  sbthom  16918  repiecef  16924  cvgcmp2nlemabs  16928  trilpo  16939  iswomni0  16948  redcwlpo  16952  dceqnconst  16958  dcapnconst  16959  nconstwlpolem  16963  nconstwlpo  16964  neapmkvlem  16965  neapmkv  16966  ltlenmkv  16968  taupi  16971  gfsumval  16974  gsumgfsum  16978  alsi1d  16990  alsi2d  16991  alsc1d  16992  alsc2d  16993