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  9251  nnind  9273  nn0supp  9572  nn0ge2m1nn  9580  zleloe  9644  zapne  9672  nn0lt2  9680  suprzclex  9697  zindd  9717  uzm1  9906  uzin  9908  infregelbex  9951  elnn1uz2  9960  nn01to3  9970  divfnzn  9974  qapne  9992  xrltnsym2  10149  xaddass  10224  xleadd1a  10228  xlt2add  10235  xlesubadd  10238  iooval2  10270  icoshftf1o  10346  fztri3or  10396  fzneuz  10460  4fvwrd4  10499  elfzo0  10545  infssuzex  10618  infssuzcldc  10620  infssfzcldc  10621  infssfzledc  10622  suprzubdc  10623  nninfdcex  10624  zsupssdc  10625  exbtwnzlemex  10636  ioom  10647  fzfig  10819  uzennn  10825  uzsinds  10833  iseqovex  10847  seq3val  10849  seqvalcd  10850  seqf  10853  seqovcd  10856  monoord2  10875  iseqf1olemjpcl  10897  iseqf1olemqpcl  10898  seq3f1olemqsum  10902  seq3f1o  10906  seqf1og  10910  seq3distr  10921  expp1  10935  expcl2lemap  10940  expclzap  10953  expap0i  10960  nn0ltexp2  11099  bcval5  11153  hashinfuni  11168  hashennnuni  11170  hashnncl  11186  resunimafz0  11226  zfz1isolemiso  11239  zfz1isolem1  11240  zfz1iso  11241  wrdsymb0  11285  wrdlen1  11290  ccat1st1st  11357  swrdrlen  11381  pfxid  11406  pfxwrdsymbg  11410  pfxtrcfv  11413  pfxccat1  11422  pfxpfxid  11429  pfxcctswrd  11430  swrdccatin1  11445  pfxccatin12  11453  pfxccatid  11461  seq3shft  11551  cvg1nlemcau  11698  rexanuz  11702  resqrexlemoverl  11735  resqrexlemglsq  11736  resqrexlemsqa  11738  resqrexlemex  11739  rersqreu  11742  caubnd2  11831  maxleast  11927  fimaxre2  11941  minmax  11944  xrmaxiflemcl  11959  xrmaxiflemab  11961  xrmaxiflemlub  11962  xrmaxadd  11975  xrminmax  11979  xrbdtri  11990  climreu  12011  reccn2ap  12027  iserex  12053  climcvg1nlem  12063  serf0  12066  fz1f1o  12089  summodclem3  12095  zsumdc  12099  fsum3  12102  isumz  12104  isumss  12106  isumss2  12108  fsumsersdc  12110  fsum3ser  12112  fsumsplit  12122  isumclim2  12137  isumclim3  12138  fsum2dlemstep  12149  fsumcnv  12152  fisumcom2  12153  bcxmas  12204  isumle  12210  cvgratnnlemnexp  12239  cvgratnnlemmn  12240  cvgratz  12247  mertenslemub  12249  mertenslemi1  12250  mertenslem2  12251  mertensabs  12252  zproddc  12294  prod1dc  12301  fprodsplitdc  12311  fprodsplit  12312  fprodunsn  12319  fprodcl2lem  12320  fprodcllemf  12328  fprod2dlemstep  12337  fprodcnv  12340  fprodcom2fi  12341  fprodle  12355  ef0lem  12375  fsumdvds  12557  mod2eq1n2dvds  12594  ndvdssub  12645  bitsfzolem  12669  bitsfzo  12670  bitsinv1  12677  gcdsupex  12682  gcdsupcl  12683  bezoutlemnewy  12721  bezoutlemmain  12723  bezoutlembi  12730  bezoutlemeu  12732  bezoutlemle  12733  uzwodc  12762  nnwofdc  12763  nnwosdc  12764  nninfctlemfo  12765  nninfct  12766  nn0seqcvgd  12767  eucalgf  12781  eucalginv  12782  lcmval  12789  prmind2  12846  dfphi2  12946  phiprmpw  12948  phimullem  12951  eulerthlem1  12953  eulerthlemrprm  12955  eulerthlema  12956  eulerthlemh  12957  eulerthlemth  12958  eulerth  12959  phisum  12967  odzcllem  12969  odzdvds  12972  pythagtriplem19  13009  pclemub  13014  pcprecl  13016  pceu  13022  pcqmul  13030  pcqcl  13033  pcxnn0cl  13037  pcxqcl  13039  pcge0  13040  pcdvdsb  13047  pceq0  13049  pcneg  13052  pcdvdstr  13054  pcgcd1  13055  pc2dvds  13057  pcz  13059  pcprmpw2  13060  pcaddlem  13066  pcadd  13067  pcmptcl  13069  pcmpt  13070  pcmptdvds  13072  fldivp1  13075  qexpz  13079  pockthlem  13083  pockthg  13084  prmunb  13089  1arith  13094  4sqlemffi  13123  4sqlem17  13134  4sqlem18  13135  4sqlem19  13136  ballotfilemcdc  13171  ballotfilem2  13176  ballotfilemfp1  13179  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemfmpn  13182  ballotfilemefi  13185  ballotfilemiex  13192  ballotfilemro  13214  ennnfonelemom  13247  ennnfoneleminc  13250  ennnfonelemhf1o  13252  ennnfonelemex  13253  ennnfonelemhom  13254  ennnfonelemdm  13259  ennnfonelemr  13262  ennnfonelemim  13263  exmidunben  13265  ctinfom  13267  inffinp1  13268  ctinf  13269  enctlem  13271  ctiunctlemu1st  13273  ctiunctlemu2nd  13274  ctiunctlemudc  13276  ctiunct  13279  ctiunctal  13280  unct  13281  ssomct  13284  nninfdclemcl  13287  nninfdclemp1  13289  nninfdc  13292  structcnvcnv  13316  setscom  13340  relelbasov  13363  ressbas2d  13369  ressval3d  13373  ressabsg  13377  restid2  13549  imasaddfnlemg  13582  quslem  13592  ercpbl  13599  fnpr2ob  13608  mgmplusf  13633  grpinvalem  13652  grpinva  13653  grprida  13654  fngsum  13655  igsumvalx  13656  gsum0g  13663  gsumval2  13664  ismnd  13684  mhmpropd  13725  grppropd  13776  grpsubf  13838  dfgrp3mlem  13857  mulgnn0p1  13890  mulgnn0subcl  13892  mulgsubcl  13893  mulgneg  13897  mulgnn0dir  13909  mulgnn0ass  13915  submmulg  13923  issubg2m  13946  issubg4m  13950  ghmmulg  14013  ghmrn  14014  gfsumval  14106  gsumgfsum  14110  lringuplu  14445  rrgsupp  14516  opprdrng  14562  lmodscaf  14588  lssintclm  14662  lspun0  14703  lidlbas  14756  psrbagconcl  14957  psr1clfi  14973  topontopon  15015  eltg3i  15051  epttop  15085  difopn  15103  uncld  15108  0nnei  15148  resttopon  15166  restabs  15170  restopnb  15176  lmcvg  15212  cnptopco  15217  cnss1  15221  cnss2  15222  cncnpi  15223  cncnp2m  15226  cnrest  15230  cnrest2  15231  cnrest2r  15232  cnptoprest  15234  cnptoprest2  15235  lmss  15241  lmff  15244  lmtopcnp  15245  lmcn  15246  txbasval  15262  upxp  15267  txcnmpt  15268  txdis1cn  15273  txlm  15274  lmcn2  15275  cnmpt11  15278  cnmpt11f  15279  cnmpt1t  15280  cnmpt12  15282  cnmpt21  15286  cnmpt21f  15287  cnmpt2t  15288  cnmpt22  15289  cnmpt22f  15290  cnmptcom  15293  hmeocnv  15302  hmeof1o  15304  hmeores  15310  txhmeo  15314  txswaphmeo  15316  isxmet2d  15343  blfvalps  15380  xblss2ps  15399  xblss2  15400  blfps  15404  blf  15405  unirnblps  15417  unirnbl  15418  isxms2  15447  bdxmet  15496  bdmet  15497  xmetxp  15502  xmettx  15505  blssioo  15548  tgioo  15549  mulcncflem  15602  divcncfap  15609  dedekindeulemuub  15612  dedekindeulemub  15613  dedekindeulemloc  15614  dedekindeulemlu  15616  suplociccreex  15619  suplociccex  15620  dedekindicclemuub  15621  dedekindicclemub  15622  dedekindicclemloc  15623  dedekindicclemlu  15625  dedekindicc  15628  ivthinclemlopn  15631  ivthinclemuopn  15633  ivthdich  15648  limcrcl  15653  limcmpted  15658  limccnp2lem  15671  limccnp2cntop  15672  limccoap  15673  dvrecap  15708  plyaddlem1  15742  plymullem1  15743  plycoeid3  15752  plyco  15754  plycj  15756  plyrecj  15758  dvply1  15760  dvply2g  15761  cosordlem  15844  logbgcd1irraplemexp  15963  logbgcd1irrap  15965  lgsneg1  16028  lgsdilem  16030  lgsdir2  16036  lgsdirprm  16037  lgsdir  16038  lgsne0  16041  lgsabs1  16042  lgsdirnn0  16050  lgsdinn0  16051  gausslemma2dlem1f1o  16063  gausslemma2dlem4  16067  lgseisenlem1  16073  lgsquadlem3  16082  2lgslem1a  16091  2sqlem5  16122  2sqlem7  16124  2sqlem8a  16125  2sqlem8  16126  2sqlem9  16127  gropeld  16174  grstructeld2dom  16175  uhgrm  16203  upgrm  16225  upgr1een  16249  uhgredgm  16261  edgupgren  16266  edgumgren  16267  edgusgren  16288  ausgrusgrben  16293  umgr2edg1  16334  usgredg2vlem1  16347  uhgr0enedgfi  16361  subupgr  16398  vtxedgfi  16414  vtxlpfi  16415  vtxdumgrfival  16423  vtxd0nedgbfi  16424  1hevtxdg0fi  16432  p1evtxdeqfilem  16436  wlkvtxm  16465  g0wlk0  16495  wlkres  16504  trlreslem  16514  clwwlkccatlem  16525  clwwlknnn  16537  trlsegvdeglem6  16590  eupth2lem3lem3fi  16595  eupth2lem3lem7fi  16599  eulerpathum  16606  dichmul0or  16644  bj-stand  16660  bj-charfundcALT  16719  bj-charfunbi  16721  bj-bdfindis  16857  bj-peano4  16865  strcollnfALT  16896  pw1map  16909  pwtrufal  16911  pwf1oexmid  16913  subctctexmid  16914  pw1nct  16917  nnsf  16923  nninfalllem1  16926  nninfall  16927  nninfsellemqall  16933  nnnninfen  16939  exmidsbthrlem  16942  sbthom  16946  repiecef  16952  cvgcmp2nlemabs  16956  trilpo  16967  iswomni0  16976  redcwlpo  16980  dceqnconst  16985  dcapnconst  16986  nconstwlpolem  16990  nconstwlpo  16991  neapmkvlem  16992  neapmkv  16993  ltlenmkv  16995  taupi  16998  alsi1d  17006  alsi2d  17007  alsc1d  17008  alsc2d  17009