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  736  3mix3  1194  mpjao3dan  1343  ecase23d  1386  exlimdh  1644  nexd  1661  alexnim  1696  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  2423  eqnetrrid  2433  3netr3g  2436  necomd  2488  r19.21bi  2620  nrexdv  2625  rexlimd  2647  rabbidva  2790  elisset  2817  euind  2993  rmoan  3006  reuind  3011  2rmorex  3012  spsbc  3043  spesbc  3118  eldifad  3211  eldifbd  3212  3sstr3g  3269  sseqtrdi  3275  difindiss  3461  un00  3541  undifss  3575  ifcldcd  3643  disjpr2  3733  difprsn1  3812  diftpsn3  3814  difsnss  3819  sneqr  3843  preqr1  3851  preq12b  3853  oprcl  3886  intab  3957  riinm  4043  rintm  4063  disjiun  4083  sndisj  4084  3brtr3g  4121  trint  4202  iinexgm  4244  exmidexmid  4286  exmid01  4288  pwntru  4289  exmid1stab  4298  pwel  4310  exss  4319  0nelop  4340  euotd  4347  opelopabsb  4354  pwunim  4383  issod  4416  frind  4449  suctr  4518  orduniss  4522  onelini  4527  oneluni  4528  eusv2i  4552  rexxfrd  4560  rabxfrd  4566  reuhypd  4568  iunpw  4577  sucexg  4596  ordsucim  4598  ordtriexmidlem  4617  ontriexmidim  4620  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  ordsucunielexmid  4629  orddif  4645  suc11g  4655  onintexmid  4671  reg3exmidlemwe  4677  tfisi  4685  peano1  4692  peano2  4693  finds2  4699  omsinds  4720  brrelex12  4764  brel  4778  ssrel  4814  ssrel2  4816  ssrelrel  4826  elrel  4828  xpsspw  4838  relop  4880  dmxpm  4952  opelresi  5024  mptimass  5089  ndmima  5113  poirr2  5129  xpmlem  5157  xpimasn  5185  iotass  5304  iotacl  5311  dffun5r  5338  funeu  5351  funeu2  5352  funfnd  5357  funopg  5360  funun  5371  fununfun  5373  funinsn  5379  funtp  5383  funcnvuni  5399  funcnvres2  5405  imadiflem  5409  imadif  5410  funimaexglem  5413  fneu2  5437  fnimaeq0  5454  fnmpt  5459  fun2  5509  f00  5528  f0bi  5529  fimadmfo  5568  foimacnv  5601  resdif  5605  f1ococnv1  5612  fv3  5662  relelfvdm  5671  elfvm  5672  nfvres  5675  dffn5im  5691  mptfvex  5732  fvmptdf  5734  fvmptdv2  5736  fndmdif  5752  dff4im  5793  fmpt  5797  fmptd  5801  fmptdf  5804  f1oresrab  5812  fcoconst  5818  fsn  5819  funopsn  5830  ftpg  5838  fsnunf  5854  resfunexg  5875  isores1  5955  riota2df  5993  acexmidlemcase  6013  brabvv  6067  funoprabg  6120  fnovim  6130  ovmpodf  6153  ovi3  6159  elmpocl  6217  uchoice  6300  1stcof  6326  2ndcof  6327  opabn1stprc  6358  fnmpo  6367  fmpoco  6381  fo2ndf  6392  f1o2ndf1  6393  disjxp1  6401  brtpos2  6417  reldmtpos  6419  dftpos3  6428  dftpos4  6429  tpostpos2  6431  tposf2  6434  tposf12  6435  tposfo  6437  tposf  6438  smores2  6460  tfrlem1  6474  tfrlem3-2d  6478  tfrlemisucaccv  6491  tfrlemibxssdm  6493  tfrlemibfn  6494  tfrlemi1  6498  tfrexlem  6500  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemaccex  6514  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemaccex  6527  tfrcldm  6529  rdgivallem  6547  rdgisucinc  6551  frecabex  6564  frecfnom  6567  frecfcllem  6570  frecsuclem  6572  omsuc  6640  nntri2  6662  nnsucuniel  6663  nnsseleq  6669  nnm00  6698  ecexr  6707  swoer  6730  elqsn0m  6772  iinerm  6776  erinxp  6778  ecinxp  6779  eroveu  6795  eroprf  6797  mapprc  6821  mapsn  6859  ixpprc  6888  ixp0  6900  resixp  6902  elixpsn  6904  dom2lem  6945  fundmen  6981  1dom1el  6993  dom0  7024  xpf1o  7030  mapxpen  7034  xpmapenlem  7035  ssenen  7037  nneneq  7043  ssfilem  7062  ssfilemd  7064  dif1en  7068  dif1enen  7069  fin0  7074  fin0or  7075  diffitest  7076  diffisn  7082  ac6sfi  7087  fimax2gtrilemstep  7090  fimax2gtri  7091  finexdc  7092  eqsndc  7095  exmidpweq  7101  pw1fin  7102  onunsnss  7109  unsnfidcel  7113  undifdcss  7115  undifdc  7116  tpfidceq  7122  fiintim  7123  fisseneq  7127  fidcenumlemr  7154  sbthlemi4  7159  sbthlemi5  7160  sbthlemi9  7164  fifo  7179  suplubti  7199  supelti  7201  infmoti  7227  infisoti  7231  djulclb  7254  updjud  7281  omp1eomlem  7293  0ct  7306  ctmlemr  7307  ctssdclemn0  7309  ctssdccl  7310  ctssdc  7312  enumct  7314  nninfninc  7322  nnnninfeq2  7328  finomni  7339  fodjuomnilemdc  7343  fodjum  7345  fodjuomnilemres  7347  fodjumkvlemres  7358  omniwomnimkv  7366  nninfwlporlem  7372  nninfwlpoimlemginf  7375  nninfwlpoim  7378  nninfinfwlpo  7379  ficardon  7393  pr2cv1  7400  exmidonfinlem  7404  en2eleq  7406  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  exmidfodomrlemim  7412  finacn  7419  acfun  7422  exmidaclem  7423  exmidontriimlem3  7438  exmidontriimlem4  7439  exmidontriim  7440  pw1if  7443  pw1on  7444  dftap2  7470  2omotaplemst  7477  exmidapne  7479  ccfunen  7483  cc1  7484  cc2lem  7485  cc2  7486  cc3  7487  acnccim  7491  elni2  7534  indpi  7562  distrnqg  7607  subhalfnqq  7634  enq0sym  7652  enq0ref  7653  enq0tr  7654  nqnq0pi  7658  nnnq0lem1  7666  distrnq0  7679  elinp  7694  elnp1st2nd  7696  prltlu  7707  prnmaxl  7708  prnminu  7709  prarloc  7723  nqprm  7762  appdivnq  7783  prmuloc  7786  mullocpr  7791  distrlem4prl  7804  distrlem4pru  7805  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemopu  7823  cauappcvgprlemopl  7866  cauappcvgprlemopu  7868  cauappcvgprlemdisj  7871  cauappcvgprlem2  7880  cauappcvgprlemlim  7881  caucvgprlemnkj  7886  caucvgprlemopl  7889  caucvgprlemopu  7891  caucvgprlemdisj  7894  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem2  7900  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemlol  7918  caucvgprprlemexbt  7926  caucvgprprlem1  7929  suplocexprlemrl  7937  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  suplocexprlemlub  7944  prsrlem1  7962  gt0srpr  7968  caucvgsrlemcl  8009  caucvgsrlembound  8014  caucvgsrlemgt1  8015  suplocsrlemb  8026  suplocsrlem  8028  suplocsr  8029  ltresr  8059  nnindnn  8113  axcaucvglemcl  8115  axcaucvglemval  8117  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  sup3exmid  9137  nnind  9159  nn0supp  9454  nn0ge2m1nn  9462  zleloe  9526  zapne  9554  nn0lt2  9561  suprzclex  9578  zindd  9598  uzm1  9787  uzin  9789  infregelbex  9832  elnn1uz2  9841  nn01to3  9851  divfnzn  9855  qapne  9873  xrltnsym2  10029  xaddass  10104  xleadd1a  10108  xlt2add  10115  xlesubadd  10118  iooval2  10150  icoshftf1o  10226  fztri3or  10274  fzneuz  10336  4fvwrd4  10375  elfzo0  10421  infssuzex  10494  infssuzcldc  10496  suprzubdc  10497  nninfdcex  10498  zsupssdc  10499  exbtwnzlemex  10510  ioom  10521  fzfig  10693  uzennn  10699  uzsinds  10707  iseqovex  10721  seq3val  10723  seqvalcd  10724  seqf  10727  seqovcd  10730  monoord2  10749  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  seq3f1olemqsum  10776  seq3f1o  10780  seqf1og  10784  seq3distr  10795  expp1  10809  expcl2lemap  10814  expclzap  10827  expap0i  10834  nn0ltexp2  10972  bcval5  11026  hashinfuni  11040  hashennnuni  11042  hashnncl  11058  resunimafz0  11096  zfz1isolemiso  11104  zfz1isolem1  11105  zfz1iso  11106  wrdsymb0  11150  wrdlen1  11155  ccat1st1st  11222  swrdrlen  11246  pfxid  11271  pfxwrdsymbg  11275  pfxtrcfv  11278  pfxccat1  11287  pfxpfxid  11294  pfxcctswrd  11295  swrdccatin1  11310  pfxccatin12  11318  pfxccatid  11326  seq3shft  11403  cvg1nlemcau  11549  rexanuz  11553  resqrexlemoverl  11586  resqrexlemglsq  11587  resqrexlemsqa  11589  resqrexlemex  11590  rersqreu  11593  caubnd2  11682  maxleast  11778  fimaxre2  11792  minmax  11795  xrmaxiflemcl  11810  xrmaxiflemab  11812  xrmaxiflemlub  11813  xrmaxadd  11826  xrminmax  11830  xrbdtri  11841  climreu  11862  reccn2ap  11878  iserex  11904  climcvg1nlem  11914  serf0  11917  fz1f1o  11940  summodclem3  11946  zsumdc  11950  fsum3  11953  isumz  11955  isumss  11957  isumss2  11959  fsumsersdc  11961  fsum3ser  11963  fsumsplit  11973  isumclim2  11988  isumclim3  11989  fsum2dlemstep  12000  fsumcnv  12003  fisumcom2  12004  bcxmas  12055  isumle  12061  cvgratnnlemnexp  12090  cvgratnnlemmn  12091  cvgratz  12098  mertenslemub  12100  mertenslemi1  12101  mertenslem2  12102  mertensabs  12103  zproddc  12145  prod1dc  12152  fprodsplitdc  12162  fprodsplit  12163  fprodunsn  12170  fprodcl2lem  12171  fprodcllemf  12179  fprod2dlemstep  12188  fprodcnv  12191  fprodcom2fi  12192  fprodle  12206  ef0lem  12226  fsumdvds  12408  mod2eq1n2dvds  12445  ndvdssub  12496  bitsfzolem  12520  bitsfzo  12521  bitsinv1  12528  gcdsupex  12533  gcdsupcl  12534  bezoutlemnewy  12572  bezoutlemmain  12574  bezoutlembi  12581  bezoutlemeu  12583  bezoutlemle  12584  uzwodc  12613  nnwofdc  12614  nnwosdc  12615  nninfctlemfo  12616  nninfct  12617  nn0seqcvgd  12618  eucalgf  12632  eucalginv  12633  lcmval  12640  prmind2  12697  dfphi2  12797  phiprmpw  12799  phimullem  12802  eulerthlem1  12804  eulerthlemrprm  12806  eulerthlema  12807  eulerthlemh  12808  eulerthlemth  12809  eulerth  12810  phisum  12818  odzcllem  12820  odzdvds  12823  pythagtriplem19  12860  pclemub  12865  pcprecl  12867  pceu  12873  pcqmul  12881  pcqcl  12884  pcxnn0cl  12888  pcxqcl  12890  pcge0  12891  pcdvdsb  12898  pceq0  12900  pcneg  12903  pcdvdstr  12905  pcgcd1  12906  pc2dvds  12908  pcz  12910  pcprmpw2  12911  pcaddlem  12917  pcadd  12918  pcmptcl  12920  pcmpt  12921  pcmptdvds  12923  fldivp1  12926  qexpz  12930  pockthlem  12934  pockthg  12935  prmunb  12940  1arith  12945  4sqlemffi  12974  4sqlem17  12985  4sqlem18  12986  4sqlem19  12987  ennnfonelemom  13034  ennnfoneleminc  13037  ennnfonelemhf1o  13039  ennnfonelemex  13040  ennnfonelemhom  13041  ennnfonelemdm  13046  ennnfonelemr  13049  ennnfonelemim  13050  exmidunben  13052  ctinfom  13054  inffinp1  13055  ctinf  13056  enctlem  13058  ctiunctlemu1st  13060  ctiunctlemu2nd  13061  ctiunctlemudc  13063  ctiunct  13066  ctiunctal  13067  unct  13068  ssomct  13071  nninfdclemcl  13074  nninfdclemp1  13076  nninfdc  13079  structcnvcnv  13103  setscom  13127  relelbasov  13150  ressbas2d  13156  ressval3d  13160  ressabsg  13164  restid2  13336  imasaddfnlemg  13402  quslem  13412  ercpbl  13419  fnpr2ob  13428  mgmplusf  13454  grpinvalem  13473  grpinva  13474  grprida  13475  fngsum  13476  igsumvalx  13477  gsum0g  13484  gsumval2  13485  ismnd  13507  mhmpropd  13554  grppropd  13605  grpsubf  13667  dfgrp3mlem  13686  mulgnn0p1  13725  mulgnn0subcl  13727  mulgsubcl  13728  mulgneg  13732  mulgnn0dir  13744  mulgnn0ass  13750  submmulg  13758  issubg2m  13781  issubg4m  13785  ghmmulg  13848  ghmrn  13849  lringuplu  14216  lmodscaf  14330  lssintclm  14404  lspun0  14445  lidlbas  14498  psr1clfi  14708  topontopon  14750  eltg3i  14786  epttop  14820  difopn  14838  uncld  14843  0nnei  14883  resttopon  14901  restabs  14905  restopnb  14911  lmcvg  14947  cnptopco  14952  cnss1  14956  cnss2  14957  cncnpi  14958  cncnp2m  14961  cnrest  14965  cnrest2  14966  cnrest2r  14967  cnptoprest  14969  cnptoprest2  14970  lmss  14976  lmff  14979  lmtopcnp  14980  lmcn  14981  txbasval  14997  upxp  15002  txcnmpt  15003  txdis1cn  15008  txlm  15009  lmcn2  15010  cnmpt11  15013  cnmpt11f  15014  cnmpt1t  15015  cnmpt12  15017  cnmpt21  15021  cnmpt21f  15022  cnmpt2t  15023  cnmpt22  15024  cnmpt22f  15025  cnmptcom  15028  hmeocnv  15037  hmeof1o  15039  hmeores  15045  txhmeo  15049  txswaphmeo  15051  isxmet2d  15078  blfvalps  15115  xblss2ps  15134  xblss2  15135  blfps  15139  blf  15140  unirnblps  15152  unirnbl  15153  isxms2  15182  bdxmet  15231  bdmet  15232  xmetxp  15237  xmettx  15240  blssioo  15283  tgioo  15284  mulcncflem  15337  divcncfap  15344  dedekindeulemuub  15347  dedekindeulemub  15348  dedekindeulemloc  15349  dedekindeulemlu  15351  suplociccreex  15354  suplociccex  15355  dedekindicclemuub  15356  dedekindicclemub  15357  dedekindicclemloc  15358  dedekindicclemlu  15360  dedekindicc  15363  ivthinclemlopn  15366  ivthinclemuopn  15368  ivthdich  15383  limcrcl  15388  limcmpted  15393  limccnp2lem  15406  limccnp2cntop  15407  limccoap  15408  dvrecap  15443  plyaddlem1  15477  plymullem1  15478  plycoeid3  15487  plyco  15489  plycj  15491  plyrecj  15493  dvply1  15495  dvply2g  15496  cosordlem  15579  logbgcd1irraplemexp  15698  logbgcd1irrap  15700  lgsneg1  15760  lgsdilem  15762  lgsdir2  15768  lgsdirprm  15769  lgsdir  15770  lgsne0  15773  lgsabs1  15774  lgsdirnn0  15782  lgsdinn0  15783  gausslemma2dlem1f1o  15795  gausslemma2dlem4  15799  lgseisenlem1  15805  lgsquadlem3  15814  2lgslem1a  15823  2sqlem5  15854  2sqlem7  15856  2sqlem8a  15857  2sqlem8  15858  2sqlem9  15859  gropeld  15906  grstructeld2dom  15907  uhgrm  15935  upgrm  15957  upgr1een  15981  uhgredgm  15993  edgupgren  15998  edgumgren  15999  edgusgren  16020  ausgrusgrben  16025  umgr2edg1  16066  usgredg2vlem1  16079  uhgr0enedgfi  16093  subupgr  16130  vtxedgfi  16146  vtxlpfi  16147  vtxdumgrfival  16155  vtxd0nedgbfi  16156  1hevtxdg0fi  16164  p1evtxdeqfilem  16168  wlkvtxm  16197  g0wlk0  16227  wlkres  16236  trlreslem  16246  clwwlkccatlem  16257  clwwlknnn  16269  trlsegvdeglem6  16322  eupth2lem3lem3fi  16327  eupth2lem3lem7fi  16331  eulerpathum  16338  bj-stand  16370  bj-charfundcALT  16430  bj-charfunbi  16432  bj-bdfindis  16568  bj-peano4  16576  strcollnfALT  16607  2omap  16620  pw1map  16622  pwtrufal  16624  pwf1oexmid  16626  subctctexmid  16627  pw1nct  16630  nnsf  16633  nninfalllem1  16636  nninfall  16637  nninfsellemqall  16643  nnnninfen  16649  exmidsbthrlem  16652  sbthom  16656  cvgcmp2nlemabs  16662  trilpo  16673  iswomni0  16681  redcwlpo  16685  dceqnconst  16690  dcapnconst  16691  nconstwlpolem  16695  nconstwlpo  16696  neapmkvlem  16697  neapmkv  16698  ltlenmkv  16700  taupi  16703  gfsumval  16706  gsumgfsum  16710  alsi1d  16721  alsi2d  16722  alsc1d  16723  alsc2d  16724