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  1809  sbh  1824  sbcof2  1858  sbidm  1899  sb6rf  1901  nfsbt  2029  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  eu2  2124  2euex  2167  eqcomd  2237  3eltr3g  2316  abbid  2348  neneqd  2424  eqnetrrid  2434  3netr3g  2437  necomd  2489  r19.21bi  2621  nrexdv  2626  rexlimd  2648  rabbidva  2791  elisset  2818  euind  2994  rmoan  3007  reuind  3012  2rmorex  3013  spsbc  3044  spesbc  3119  eldifad  3212  eldifbd  3213  3sstr3g  3270  sseqtrdi  3276  difindiss  3463  un00  3543  undifss  3577  ifcldcd  3647  disjpr2  3737  difprsn1  3817  diftpsn3  3819  difsnss  3824  sneqr  3848  preqr1  3856  preq12b  3858  oprcl  3891  intab  3962  riinm  4048  rintm  4068  disjiun  4088  sndisj  4089  3brtr3g  4126  trint  4207  iinexgm  4249  exmidexmid  4292  exmid01  4294  pwntru  4295  exmid1stab  4304  pwel  4316  exss  4325  0nelop  4346  euotd  4353  opelopabsb  4360  pwunim  4389  issod  4422  frind  4455  suctr  4524  orduniss  4528  onelini  4533  oneluni  4534  eusv2i  4558  rexxfrd  4566  rabxfrd  4572  reuhypd  4574  iunpw  4583  sucexg  4602  ordsucim  4604  ordtriexmidlem  4623  ontriexmidim  4626  ordtri2or2exmidlem  4630  onsucelsucexmidlem  4633  ordsucunielexmid  4635  orddif  4651  suc11g  4661  onintexmid  4677  reg3exmidlemwe  4683  tfisi  4691  peano1  4698  peano2  4699  finds2  4705  omsinds  4726  brrelex12  4770  brel  4784  ssrel  4820  ssrel2  4822  ssrelrel  4832  elrel  4834  xpsspw  4844  relop  4886  dmxpm  4958  opelresi  5030  mptimass  5095  ndmima  5120  poirr2  5136  xpmlem  5164  xpimasn  5192  iotass  5311  iotacl  5318  dffun5r  5345  funeu  5358  funeu2  5359  funfnd  5364  funopg  5367  funun  5378  fununfun  5380  funinsn  5386  funtp  5390  funcnvuni  5406  funcnvres2  5412  imadiflem  5416  imadif  5417  funimaexglem  5420  fneu2  5444  fnimaeq0  5461  fnmpt  5466  fun2  5517  f00  5537  f0bi  5538  fimadmfo  5577  foimacnv  5610  resdif  5614  f1ococnv1  5621  fv3  5671  relelfvdm  5680  elfvm  5681  nfvres  5684  dffn5im  5700  mptfvex  5741  fvmptdf  5743  fvmptdv2  5745  fndmdif  5761  dff4im  5801  fmpt  5805  fmptd  5809  fmptdf  5812  f1oresrab  5820  fcoconst  5826  fsn  5827  funopsn  5838  ftpg  5846  fsnunf  5862  resfunexg  5883  isores1  5965  riota2df  6003  acexmidlemcase  6023  brabvv  6077  funoprabg  6130  fnovim  6140  ovmpodf  6163  ovi3  6169  elmpocl  6227  uchoice  6309  1stcof  6335  2ndcof  6336  opabn1stprc  6367  fnmpo  6376  fmpoco  6390  fo2ndf  6401  f1o2ndf1  6402  disjxp1  6410  fvdifsuppst  6422  fsuppeq  6425  fsuppeqg  6426  suppssrst  6439  suppssrgst  6440  brtpos2  6460  reldmtpos  6462  dftpos3  6471  dftpos4  6472  tpostpos2  6474  tposf2  6477  tposf12  6478  tposfo  6480  tposf  6481  smores2  6503  tfrlem1  6517  tfrlem3-2d  6521  tfrlemisucaccv  6534  tfrlemibxssdm  6536  tfrlemibfn  6537  tfrlemi1  6541  tfrexlem  6543  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemaccex  6557  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemaccex  6570  tfrcldm  6572  rdgivallem  6590  rdgisucinc  6594  frecabex  6607  frecfnom  6610  frecfcllem  6613  frecsuclem  6615  omsuc  6683  nntri2  6705  nnsucuniel  6706  nnsseleq  6712  nnm00  6741  ecexr  6750  swoer  6773  elqsn0m  6815  iinerm  6819  erinxp  6821  ecinxp  6822  eroveu  6838  eroprf  6840  mapprc  6864  mapsn  6902  ixpprc  6931  ixp0  6943  resixp  6945  elixpsn  6947  dom2lem  6988  fundmen  7024  1dom1el  7036  dom0  7067  xpf1o  7073  mapxpen  7077  xpmapenlem  7078  ssenen  7080  nneneq  7086  ssfilem  7105  ssfilemd  7107  dif1en  7111  dif1enen  7112  fin0  7117  fin0or  7118  diffitest  7119  diffisn  7125  ac6sfi  7130  fimax2gtrilemstep  7133  fimax2gtri  7134  finexdc  7135  eqsndc  7138  exmidpweq  7144  pw1fin  7145  onunsnss  7152  unsnfidcel  7156  undifdcss  7158  undifdc  7159  tpfidceq  7165  fiintim  7166  fisseneq  7170  fidcenumlemr  7197  sbthlemi4  7202  sbthlemi5  7203  sbthlemi9  7207  fifo  7222  suplubti  7242  supelti  7244  infmoti  7270  infisoti  7274  djulclb  7297  updjud  7324  omp1eomlem  7336  0ct  7349  ctmlemr  7350  ctssdclemn0  7352  ctssdccl  7353  ctssdc  7355  enumct  7357  nninfninc  7365  nnnninfeq2  7371  finomni  7382  fodjuomnilemdc  7386  fodjum  7388  fodjuomnilemres  7390  fodjumkvlemres  7401  omniwomnimkv  7409  nninfwlporlem  7415  nninfwlpoimlemginf  7418  nninfwlpoim  7421  nninfinfwlpo  7422  ficardon  7436  pr2cv1  7443  exmidonfinlem  7447  en2eleq  7449  exmidfodomrlemeldju  7453  exmidfodomrlemreseldju  7454  exmidfodomrlemim  7455  finacn  7462  acfun  7465  exmidaclem  7466  exmidontriimlem3  7481  exmidontriimlem4  7482  exmidontriim  7483  pw1if  7486  pw1on  7487  dftap2  7513  2omotaplemst  7520  exmidapne  7522  ccfunen  7526  cc1  7527  cc2lem  7528  cc2  7529  cc3  7530  acnccim  7534  elni2  7577  indpi  7605  distrnqg  7650  subhalfnqq  7677  enq0sym  7695  enq0ref  7696  enq0tr  7697  nqnq0pi  7701  nnnq0lem1  7709  distrnq0  7722  elinp  7737  elnp1st2nd  7739  prltlu  7750  prnmaxl  7751  prnminu  7752  prarloc  7766  nqprm  7805  appdivnq  7826  prmuloc  7829  mullocpr  7834  distrlem4prl  7847  distrlem4pru  7848  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemopu  7866  cauappcvgprlemopl  7909  cauappcvgprlemopu  7911  cauappcvgprlemdisj  7914  cauappcvgprlem2  7923  cauappcvgprlemlim  7924  caucvgprlemnkj  7929  caucvgprlemopl  7932  caucvgprlemopu  7934  caucvgprlemdisj  7937  caucvgprlemcl  7939  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgprlem2  7943  caucvgprprlemcbv  7950  caucvgprprlemval  7951  caucvgprprlemlol  7961  caucvgprprlemexbt  7969  caucvgprprlem1  7972  suplocexprlemrl  7980  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemub  7986  suplocexprlemlub  7987  prsrlem1  8005  gt0srpr  8011  caucvgsrlemcl  8052  caucvgsrlembound  8057  caucvgsrlemgt1  8058  suplocsrlemb  8069  suplocsrlem  8071  suplocsr  8072  ltresr  8102  nnindnn  8156  axcaucvglemcl  8158  axcaucvglemval  8160  axcaucvglemcau  8161  axcaucvglemres  8162  axpre-suploclemres  8164  axpre-suploc  8165  sup3exmid  9180  nnind  9202  nn0supp  9497  nn0ge2m1nn  9505  zleloe  9569  zapne  9597  nn0lt2  9604  suprzclex  9621  zindd  9641  uzm1  9830  uzin  9832  infregelbex  9875  elnn1uz2  9884  nn01to3  9894  divfnzn  9898  qapne  9916  xrltnsym2  10072  xaddass  10147  xleadd1a  10151  xlt2add  10158  xlesubadd  10161  iooval2  10193  icoshftf1o  10269  fztri3or  10317  fzneuz  10379  4fvwrd4  10418  elfzo0  10464  infssuzex  10537  infssuzcldc  10539  suprzubdc  10540  nninfdcex  10541  zsupssdc  10542  exbtwnzlemex  10553  ioom  10564  fzfig  10736  uzennn  10742  uzsinds  10750  iseqovex  10764  seq3val  10766  seqvalcd  10767  seqf  10770  seqovcd  10773  monoord2  10792  iseqf1olemjpcl  10814  iseqf1olemqpcl  10815  seq3f1olemqsum  10819  seq3f1o  10823  seqf1og  10827  seq3distr  10838  expp1  10852  expcl2lemap  10857  expclzap  10870  expap0i  10877  nn0ltexp2  11015  bcval5  11069  hashinfuni  11083  hashennnuni  11085  hashnncl  11101  resunimafz0  11139  zfz1isolemiso  11147  zfz1isolem1  11148  zfz1iso  11149  wrdsymb0  11193  wrdlen1  11198  ccat1st1st  11265  swrdrlen  11289  pfxid  11314  pfxwrdsymbg  11318  pfxtrcfv  11321  pfxccat1  11330  pfxpfxid  11337  pfxcctswrd  11338  swrdccatin1  11353  pfxccatin12  11361  pfxccatid  11369  seq3shft  11459  cvg1nlemcau  11605  rexanuz  11609  resqrexlemoverl  11642  resqrexlemglsq  11643  resqrexlemsqa  11645  resqrexlemex  11646  rersqreu  11649  caubnd2  11738  maxleast  11834  fimaxre2  11848  minmax  11851  xrmaxiflemcl  11866  xrmaxiflemab  11868  xrmaxiflemlub  11869  xrmaxadd  11882  xrminmax  11886  xrbdtri  11897  climreu  11918  reccn2ap  11934  iserex  11960  climcvg1nlem  11970  serf0  11973  fz1f1o  11996  summodclem3  12002  zsumdc  12006  fsum3  12009  isumz  12011  isumss  12013  isumss2  12015  fsumsersdc  12017  fsum3ser  12019  fsumsplit  12029  isumclim2  12044  isumclim3  12045  fsum2dlemstep  12056  fsumcnv  12059  fisumcom2  12060  bcxmas  12111  isumle  12117  cvgratnnlemnexp  12146  cvgratnnlemmn  12147  cvgratz  12154  mertenslemub  12156  mertenslemi1  12157  mertenslem2  12158  mertensabs  12159  zproddc  12201  prod1dc  12208  fprodsplitdc  12218  fprodsplit  12219  fprodunsn  12226  fprodcl2lem  12227  fprodcllemf  12235  fprod2dlemstep  12244  fprodcnv  12247  fprodcom2fi  12248  fprodle  12262  ef0lem  12282  fsumdvds  12464  mod2eq1n2dvds  12501  ndvdssub  12552  bitsfzolem  12576  bitsfzo  12577  bitsinv1  12584  gcdsupex  12589  gcdsupcl  12590  bezoutlemnewy  12628  bezoutlemmain  12630  bezoutlembi  12637  bezoutlemeu  12639  bezoutlemle  12640  uzwodc  12669  nnwofdc  12670  nnwosdc  12671  nninfctlemfo  12672  nninfct  12673  nn0seqcvgd  12674  eucalgf  12688  eucalginv  12689  lcmval  12696  prmind2  12753  dfphi2  12853  phiprmpw  12855  phimullem  12858  eulerthlem1  12860  eulerthlemrprm  12862  eulerthlema  12863  eulerthlemh  12864  eulerthlemth  12865  eulerth  12866  phisum  12874  odzcllem  12876  odzdvds  12879  pythagtriplem19  12916  pclemub  12921  pcprecl  12923  pceu  12929  pcqmul  12937  pcqcl  12940  pcxnn0cl  12944  pcxqcl  12946  pcge0  12947  pcdvdsb  12954  pceq0  12956  pcneg  12959  pcdvdstr  12961  pcgcd1  12962  pc2dvds  12964  pcz  12966  pcprmpw2  12967  pcaddlem  12973  pcadd  12974  pcmptcl  12976  pcmpt  12977  pcmptdvds  12979  fldivp1  12982  qexpz  12986  pockthlem  12990  pockthg  12991  prmunb  12996  1arith  13001  4sqlemffi  13030  4sqlem17  13041  4sqlem18  13042  4sqlem19  13043  ennnfonelemom  13090  ennnfoneleminc  13093  ennnfonelemhf1o  13095  ennnfonelemex  13096  ennnfonelemhom  13097  ennnfonelemdm  13102  ennnfonelemr  13105  ennnfonelemim  13106  exmidunben  13108  ctinfom  13110  inffinp1  13111  ctinf  13112  enctlem  13114  ctiunctlemu1st  13116  ctiunctlemu2nd  13117  ctiunctlemudc  13119  ctiunct  13122  ctiunctal  13123  unct  13124  ssomct  13127  nninfdclemcl  13130  nninfdclemp1  13132  nninfdc  13135  structcnvcnv  13159  setscom  13183  relelbasov  13206  ressbas2d  13212  ressval3d  13216  ressabsg  13220  restid2  13392  imasaddfnlemg  13458  quslem  13468  ercpbl  13475  fnpr2ob  13484  mgmplusf  13510  grpinvalem  13529  grpinva  13530  grprida  13531  fngsum  13532  igsumvalx  13533  gsum0g  13540  gsumval2  13541  ismnd  13563  mhmpropd  13610  grppropd  13661  grpsubf  13723  dfgrp3mlem  13742  mulgnn0p1  13781  mulgnn0subcl  13783  mulgsubcl  13784  mulgneg  13788  mulgnn0dir  13800  mulgnn0ass  13806  submmulg  13814  issubg2m  13837  issubg4m  13841  ghmmulg  13904  ghmrn  13905  lringuplu  14272  lmodscaf  14386  lssintclm  14460  lspun0  14501  lidlbas  14554  psrbagconcl  14753  psr1clfi  14769  topontopon  14811  eltg3i  14847  epttop  14881  difopn  14899  uncld  14904  0nnei  14944  resttopon  14962  restabs  14966  restopnb  14972  lmcvg  15008  cnptopco  15013  cnss1  15017  cnss2  15018  cncnpi  15019  cncnp2m  15022  cnrest  15026  cnrest2  15027  cnrest2r  15028  cnptoprest  15030  cnptoprest2  15031  lmss  15037  lmff  15040  lmtopcnp  15041  lmcn  15042  txbasval  15058  upxp  15063  txcnmpt  15064  txdis1cn  15069  txlm  15070  lmcn2  15071  cnmpt11  15074  cnmpt11f  15075  cnmpt1t  15076  cnmpt12  15078  cnmpt21  15082  cnmpt21f  15083  cnmpt2t  15084  cnmpt22  15085  cnmpt22f  15086  cnmptcom  15089  hmeocnv  15098  hmeof1o  15100  hmeores  15106  txhmeo  15110  txswaphmeo  15112  isxmet2d  15139  blfvalps  15176  xblss2ps  15195  xblss2  15196  blfps  15200  blf  15201  unirnblps  15213  unirnbl  15214  isxms2  15243  bdxmet  15292  bdmet  15293  xmetxp  15298  xmettx  15301  blssioo  15344  tgioo  15345  mulcncflem  15398  divcncfap  15405  dedekindeulemuub  15408  dedekindeulemub  15409  dedekindeulemloc  15410  dedekindeulemlu  15412  suplociccreex  15415  suplociccex  15416  dedekindicclemuub  15417  dedekindicclemub  15418  dedekindicclemloc  15419  dedekindicclemlu  15421  dedekindicc  15424  ivthinclemlopn  15427  ivthinclemuopn  15429  ivthdich  15444  limcrcl  15449  limcmpted  15454  limccnp2lem  15467  limccnp2cntop  15468  limccoap  15469  dvrecap  15504  plyaddlem1  15538  plymullem1  15539  plycoeid3  15548  plyco  15550  plycj  15552  plyrecj  15554  dvply1  15556  dvply2g  15557  cosordlem  15640  logbgcd1irraplemexp  15759  logbgcd1irrap  15761  lgsneg1  15824  lgsdilem  15826  lgsdir2  15832  lgsdirprm  15833  lgsdir  15834  lgsne0  15837  lgsabs1  15838  lgsdirnn0  15846  lgsdinn0  15847  gausslemma2dlem1f1o  15859  gausslemma2dlem4  15863  lgseisenlem1  15869  lgsquadlem3  15878  2lgslem1a  15887  2sqlem5  15918  2sqlem7  15920  2sqlem8a  15921  2sqlem8  15922  2sqlem9  15923  gropeld  15970  grstructeld2dom  15971  uhgrm  15999  upgrm  16021  upgr1een  16045  uhgredgm  16057  edgupgren  16062  edgumgren  16063  edgusgren  16084  ausgrusgrben  16089  umgr2edg1  16130  usgredg2vlem1  16143  uhgr0enedgfi  16157  subupgr  16194  vtxedgfi  16210  vtxlpfi  16211  vtxdumgrfival  16219  vtxd0nedgbfi  16220  1hevtxdg0fi  16228  p1evtxdeqfilem  16232  wlkvtxm  16261  g0wlk0  16291  wlkres  16300  trlreslem  16310  clwwlkccatlem  16321  clwwlknnn  16333  trlsegvdeglem6  16386  eupth2lem3lem3fi  16391  eupth2lem3lem7fi  16395  eulerpathum  16402  bj-stand  16446  bj-charfundcALT  16505  bj-charfunbi  16507  bj-bdfindis  16643  bj-peano4  16651  strcollnfALT  16682  2omap  16695  pw1map  16697  pwtrufal  16699  pwf1oexmid  16701  subctctexmid  16702  pw1nct  16705  nnsf  16711  nninfalllem1  16714  nninfall  16715  nninfsellemqall  16721  nnnninfen  16727  exmidsbthrlem  16730  sbthom  16734  repiecef  16740  cvgcmp2nlemabs  16744  trilpo  16755  iswomni0  16764  redcwlpo  16768  dceqnconst  16773  dcapnconst  16774  nconstwlpolem  16778  nconstwlpo  16779  neapmkvlem  16780  neapmkv  16781  ltlenmkv  16783  taupi  16786  gfsumval  16789  gsumgfsum  16793  alsi1d  16804  alsi2d  16805  alsc1d  16806  alsc2d  16807