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  734  3mix3  1192  mpjao3dan  1341  ecase23d  1384  exlimdh  1642  nexd  1659  alexnim  1694  excomim  1709  19.41  1732  equcomd  1753  nfexd  1807  sbh  1822  sbcof2  1856  sbidm  1897  sb6rf  1899  nfsbt  2027  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  eu2  2122  2euex  2165  eqcomd  2235  3eltr3g  2314  abbid  2346  neneqd  2421  eqnetrrid  2431  3netr3g  2434  necomd  2486  r19.21bi  2618  nrexdv  2623  rexlimd  2645  rabbidva  2787  elisset  2814  euind  2990  rmoan  3003  reuind  3008  2rmorex  3009  spsbc  3040  spesbc  3115  eldifad  3208  eldifbd  3209  3sstr3g  3266  sseqtrdi  3272  difindiss  3458  un00  3538  undifss  3572  ifcldcd  3640  disjpr2  3730  difprsn1  3807  diftpsn3  3809  difsnss  3814  sneqr  3838  preqr1  3846  preq12b  3848  oprcl  3881  intab  3952  riinm  4038  rintm  4058  disjiun  4078  sndisj  4079  3brtr3g  4116  trint  4197  iinexgm  4238  exmidexmid  4280  exmid01  4282  pwntru  4283  exmid1stab  4292  pwel  4304  exss  4313  0nelop  4334  euotd  4341  opelopabsb  4348  pwunim  4377  issod  4410  frind  4443  suctr  4512  orduniss  4516  onelini  4521  oneluni  4522  eusv2i  4546  rexxfrd  4554  rabxfrd  4560  reuhypd  4562  iunpw  4571  sucexg  4590  ordsucim  4592  ordtriexmidlem  4611  ontriexmidim  4614  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  ordsucunielexmid  4623  orddif  4639  suc11g  4649  onintexmid  4665  reg3exmidlemwe  4671  tfisi  4679  peano1  4686  peano2  4687  finds2  4693  omsinds  4714  brrelex12  4757  brel  4771  ssrel  4807  ssrel2  4809  ssrelrel  4819  elrel  4821  xpsspw  4831  relop  4872  dmxpm  4944  opelresi  5016  mptimass  5081  ndmima  5105  poirr2  5121  xpmlem  5149  xpimasn  5177  iotass  5296  iotacl  5303  dffun5r  5330  funeu  5343  funeu2  5344  funfnd  5349  funopg  5352  funun  5362  fununfun  5364  funinsn  5370  funtp  5374  funcnvuni  5390  funcnvres2  5396  imadiflem  5400  imadif  5401  funimaexglem  5404  fneu2  5428  fnimaeq0  5445  fnmpt  5450  fun2  5500  f00  5519  f0bi  5520  fimadmfo  5559  foimacnv  5592  resdif  5596  f1ococnv1  5603  fv3  5652  relelfvdm  5661  elfvm  5662  nfvres  5665  dffn5im  5681  mptfvex  5722  fvmptdf  5724  fvmptdv2  5726  fndmdif  5742  dff4im  5783  fmpt  5787  fmptd  5791  fmptdf  5794  f1oresrab  5802  fcoconst  5808  fsn  5809  funopsn  5819  ftpg  5827  fsnunf  5843  resfunexg  5864  isores1  5944  riota2df  5982  acexmidlemcase  6002  brabvv  6056  funoprabg  6109  fnovim  6119  ovmpodf  6142  ovi3  6148  elmpocl  6206  uchoice  6289  1stcof  6315  2ndcof  6316  fnmpo  6354  fmpoco  6368  fo2ndf  6379  f1o2ndf1  6380  disjxp1  6388  brtpos2  6403  reldmtpos  6405  dftpos3  6414  dftpos4  6415  tpostpos2  6417  tposf2  6420  tposf12  6421  tposfo  6423  tposf  6424  smores2  6446  tfrlem1  6460  tfrlem3-2d  6464  tfrlemisucaccv  6477  tfrlemibxssdm  6479  tfrlemibfn  6480  tfrlemi1  6484  tfrexlem  6486  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemaccex  6500  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemaccex  6513  tfrcldm  6515  rdgivallem  6533  rdgisucinc  6537  frecabex  6550  frecfnom  6553  frecfcllem  6556  frecsuclem  6558  omsuc  6626  nntri2  6648  nnsucuniel  6649  nnsseleq  6655  nnm00  6684  ecexr  6693  swoer  6716  elqsn0m  6758  iinerm  6762  erinxp  6764  ecinxp  6765  eroveu  6781  eroprf  6783  mapprc  6807  mapsn  6845  ixpprc  6874  ixp0  6886  resixp  6888  elixpsn  6890  dom2lem  6931  fundmen  6967  dom0  7007  xpf1o  7013  mapxpen  7017  xpmapenlem  7018  ssenen  7020  nneneq  7026  ssfilem  7045  dif1en  7049  dif1enen  7050  fin0  7055  fin0or  7056  diffitest  7057  diffisn  7063  ac6sfi  7068  fimax2gtrilemstep  7070  fimax2gtri  7071  finexdc  7072  exmidpweq  7079  pw1fin  7080  onunsnss  7087  unsnfidcel  7091  undifdcss  7093  undifdc  7094  tpfidceq  7100  fiintim  7101  fisseneq  7104  fidcenumlemr  7130  sbthlemi4  7135  sbthlemi5  7136  sbthlemi9  7140  fifo  7155  suplubti  7175  supelti  7177  infmoti  7203  infisoti  7207  djulclb  7230  updjud  7257  omp1eomlem  7269  0ct  7282  ctmlemr  7283  ctssdclemn0  7285  ctssdccl  7286  ctssdc  7288  enumct  7290  nninfninc  7298  nnnninfeq2  7304  finomni  7315  fodjuomnilemdc  7319  fodjum  7321  fodjuomnilemres  7323  fodjumkvlemres  7334  omniwomnimkv  7342  nninfwlporlem  7348  nninfwlpoimlemginf  7351  nninfwlpoim  7354  nninfinfwlpo  7355  ficardon  7369  pr2cv1  7376  exmidonfinlem  7379  en2eleq  7381  exmidfodomrlemeldju  7385  exmidfodomrlemreseldju  7386  exmidfodomrlemim  7387  finacn  7394  acfun  7397  exmidaclem  7398  exmidontriimlem3  7413  exmidontriimlem4  7414  exmidontriim  7415  pw1if  7418  pw1on  7419  dftap2  7445  2omotaplemst  7452  exmidapne  7454  ccfunen  7458  cc1  7459  cc2lem  7460  cc2  7461  cc3  7462  acnccim  7466  elni2  7509  indpi  7537  distrnqg  7582  subhalfnqq  7609  enq0sym  7627  enq0ref  7628  enq0tr  7629  nqnq0pi  7633  nnnq0lem1  7641  distrnq0  7654  elinp  7669  elnp1st2nd  7671  prltlu  7682  prnmaxl  7683  prnminu  7684  prarloc  7698  nqprm  7737  appdivnq  7758  prmuloc  7761  mullocpr  7766  distrlem4prl  7779  distrlem4pru  7780  ltexprlemm  7795  ltexprlemopl  7796  ltexprlemopu  7798  cauappcvgprlemopl  7841  cauappcvgprlemopu  7843  cauappcvgprlemdisj  7846  cauappcvgprlem2  7855  cauappcvgprlemlim  7856  caucvgprlemnkj  7861  caucvgprlemopl  7864  caucvgprlemopu  7866  caucvgprlemdisj  7869  caucvgprlemcl  7871  caucvgprlemladdfu  7872  caucvgprlemladdrl  7873  caucvgprlem2  7875  caucvgprprlemcbv  7882  caucvgprprlemval  7883  caucvgprprlemlol  7893  caucvgprprlemexbt  7901  caucvgprprlem1  7904  suplocexprlemrl  7912  suplocexprlemmu  7913  suplocexprlemru  7914  suplocexprlemdisj  7915  suplocexprlemloc  7916  suplocexprlemub  7918  suplocexprlemlub  7919  prsrlem1  7937  gt0srpr  7943  caucvgsrlemcl  7984  caucvgsrlembound  7989  caucvgsrlemgt1  7990  suplocsrlemb  8001  suplocsrlem  8003  suplocsr  8004  ltresr  8034  nnindnn  8088  axcaucvglemcl  8090  axcaucvglemval  8092  axcaucvglemcau  8093  axcaucvglemres  8094  axpre-suploclemres  8096  axpre-suploc  8097  sup3exmid  9112  nnind  9134  nn0supp  9429  nn0ge2m1nn  9437  zleloe  9501  zapne  9529  nn0lt2  9536  suprzclex  9553  zindd  9573  uzm1  9761  uzin  9763  infregelbex  9801  elnn1uz2  9810  nn01to3  9820  divfnzn  9824  qapne  9842  xrltnsym2  9998  xaddass  10073  xleadd1a  10077  xlt2add  10084  xlesubadd  10087  iooval2  10119  icoshftf1o  10195  fztri3or  10243  fzneuz  10305  4fvwrd4  10344  elfzo0  10390  infssuzex  10461  infssuzcldc  10463  suprzubdc  10464  nninfdcex  10465  zsupssdc  10466  exbtwnzlemex  10477  ioom  10488  fzfig  10660  uzennn  10666  uzsinds  10674  iseqovex  10688  seq3val  10690  seqvalcd  10691  seqf  10694  seqovcd  10697  monoord2  10716  iseqf1olemjpcl  10738  iseqf1olemqpcl  10739  seq3f1olemqsum  10743  seq3f1o  10747  seqf1og  10751  seq3distr  10762  expp1  10776  expcl2lemap  10781  expclzap  10794  expap0i  10801  nn0ltexp2  10939  bcval5  10993  hashinfuni  11007  hashennnuni  11009  hashnncl  11025  resunimafz0  11061  zfz1isolemiso  11069  zfz1isolem1  11070  zfz1iso  11071  wrdsymb0  11112  wrdlen1  11117  ccat1st1st  11180  swrdrlen  11201  pfxid  11226  pfxwrdsymbg  11230  pfxtrcfv  11233  pfxccat1  11242  pfxpfxid  11249  pfxcctswrd  11250  swrdccatin1  11265  pfxccatin12  11273  pfxccatid  11281  seq3shft  11357  cvg1nlemcau  11503  rexanuz  11507  resqrexlemoverl  11540  resqrexlemglsq  11541  resqrexlemsqa  11543  resqrexlemex  11544  rersqreu  11547  caubnd2  11636  maxleast  11732  fimaxre2  11746  minmax  11749  xrmaxiflemcl  11764  xrmaxiflemab  11766  xrmaxiflemlub  11767  xrmaxadd  11780  xrminmax  11784  xrbdtri  11795  climreu  11816  reccn2ap  11832  iserex  11858  climcvg1nlem  11868  serf0  11871  fz1f1o  11894  summodclem3  11899  zsumdc  11903  fsum3  11906  isumz  11908  isumss  11910  isumss2  11912  fsumsersdc  11914  fsum3ser  11916  fsumsplit  11926  isumclim2  11941  isumclim3  11942  fsum2dlemstep  11953  fsumcnv  11956  fisumcom2  11957  bcxmas  12008  isumle  12014  cvgratnnlemnexp  12043  cvgratnnlemmn  12044  cvgratz  12051  mertenslemub  12053  mertenslemi1  12054  mertenslem2  12055  mertensabs  12056  zproddc  12098  prod1dc  12105  fprodsplitdc  12115  fprodsplit  12116  fprodunsn  12123  fprodcl2lem  12124  fprodcllemf  12132  fprod2dlemstep  12141  fprodcnv  12144  fprodcom2fi  12145  fprodle  12159  ef0lem  12179  fsumdvds  12361  mod2eq1n2dvds  12398  ndvdssub  12449  bitsfzolem  12473  bitsfzo  12474  bitsinv1  12481  gcdsupex  12486  gcdsupcl  12487  bezoutlemnewy  12525  bezoutlemmain  12527  bezoutlembi  12534  bezoutlemeu  12536  bezoutlemle  12537  uzwodc  12566  nnwofdc  12567  nnwosdc  12568  nninfctlemfo  12569  nninfct  12570  nn0seqcvgd  12571  eucalgf  12585  eucalginv  12586  lcmval  12593  prmind2  12650  dfphi2  12750  phiprmpw  12752  phimullem  12755  eulerthlem1  12757  eulerthlemrprm  12759  eulerthlema  12760  eulerthlemh  12761  eulerthlemth  12762  eulerth  12763  phisum  12771  odzcllem  12773  odzdvds  12776  pythagtriplem19  12813  pclemub  12818  pcprecl  12820  pceu  12826  pcqmul  12834  pcqcl  12837  pcxnn0cl  12841  pcxqcl  12843  pcge0  12844  pcdvdsb  12851  pceq0  12853  pcneg  12856  pcdvdstr  12858  pcgcd1  12859  pc2dvds  12861  pcz  12863  pcprmpw2  12864  pcaddlem  12870  pcadd  12871  pcmptcl  12873  pcmpt  12874  pcmptdvds  12876  fldivp1  12879  qexpz  12883  pockthlem  12887  pockthg  12888  prmunb  12893  1arith  12898  4sqlemffi  12927  4sqlem17  12938  4sqlem18  12939  4sqlem19  12940  ennnfonelemom  12987  ennnfoneleminc  12990  ennnfonelemhf1o  12992  ennnfonelemex  12993  ennnfonelemhom  12994  ennnfonelemdm  12999  ennnfonelemr  13002  ennnfonelemim  13003  exmidunben  13005  ctinfom  13007  inffinp1  13008  ctinf  13009  enctlem  13011  ctiunctlemu1st  13013  ctiunctlemu2nd  13014  ctiunctlemudc  13016  ctiunct  13019  ctiunctal  13020  unct  13021  ssomct  13024  nninfdclemcl  13027  nninfdclemp1  13029  nninfdc  13032  structcnvcnv  13056  setscom  13080  relelbasov  13103  ressbas2d  13109  ressval3d  13113  ressabsg  13117  restid2  13289  imasaddfnlemg  13355  quslem  13365  ercpbl  13372  fnpr2ob  13381  mgmplusf  13407  grpinvalem  13426  grpinva  13427  grprida  13428  fngsum  13429  igsumvalx  13430  gsum0g  13437  gsumval2  13438  ismnd  13460  mhmpropd  13507  grppropd  13558  grpsubf  13620  dfgrp3mlem  13639  mulgnn0p1  13678  mulgnn0subcl  13680  mulgsubcl  13681  mulgneg  13685  mulgnn0dir  13697  mulgnn0ass  13703  submmulg  13711  issubg2m  13734  issubg4m  13738  ghmmulg  13801  ghmrn  13802  lringuplu  14168  lmodscaf  14282  lssintclm  14356  lspun0  14397  lidlbas  14450  psr1clfi  14660  topontopon  14702  eltg3i  14738  epttop  14772  difopn  14790  uncld  14795  0nnei  14835  resttopon  14853  restabs  14857  restopnb  14863  lmcvg  14899  cnptopco  14904  cnss1  14908  cnss2  14909  cncnpi  14910  cncnp2m  14913  cnrest  14917  cnrest2  14918  cnrest2r  14919  cnptoprest  14921  cnptoprest2  14922  lmss  14928  lmff  14931  lmtopcnp  14932  lmcn  14933  txbasval  14949  upxp  14954  txcnmpt  14955  txdis1cn  14960  txlm  14961  lmcn2  14962  cnmpt11  14965  cnmpt11f  14966  cnmpt1t  14967  cnmpt12  14969  cnmpt21  14973  cnmpt21f  14974  cnmpt2t  14975  cnmpt22  14976  cnmpt22f  14977  cnmptcom  14980  hmeocnv  14989  hmeof1o  14991  hmeores  14997  txhmeo  15001  txswaphmeo  15003  isxmet2d  15030  blfvalps  15067  xblss2ps  15086  xblss2  15087  blfps  15091  blf  15092  unirnblps  15104  unirnbl  15105  isxms2  15134  bdxmet  15183  bdmet  15184  xmetxp  15189  xmettx  15192  blssioo  15235  tgioo  15236  mulcncflem  15289  divcncfap  15296  dedekindeulemuub  15299  dedekindeulemub  15300  dedekindeulemloc  15301  dedekindeulemlu  15303  suplociccreex  15306  suplociccex  15307  dedekindicclemuub  15308  dedekindicclemub  15309  dedekindicclemloc  15310  dedekindicclemlu  15312  dedekindicc  15315  ivthinclemlopn  15318  ivthinclemuopn  15320  ivthdich  15335  limcrcl  15340  limcmpted  15345  limccnp2lem  15358  limccnp2cntop  15359  limccoap  15360  dvrecap  15395  plyaddlem1  15429  plymullem1  15430  plycoeid3  15439  plyco  15441  plycj  15443  plyrecj  15445  dvply1  15447  dvply2g  15448  cosordlem  15531  logbgcd1irraplemexp  15650  logbgcd1irrap  15652  lgsneg1  15712  lgsdilem  15714  lgsdir2  15720  lgsdirprm  15721  lgsdir  15722  lgsne0  15725  lgsabs1  15726  lgsdirnn0  15734  lgsdinn0  15735  gausslemma2dlem1f1o  15747  gausslemma2dlem4  15751  lgseisenlem1  15757  lgsquadlem3  15766  2lgslem1a  15775  2sqlem5  15806  2sqlem7  15808  2sqlem8a  15809  2sqlem8  15810  2sqlem9  15811  gropeld  15858  grstructeld2dom  15859  uhgrm  15886  upgrm  15908  uhgredgm  15942  edgupgren  15947  edgumgren  15948  edgusgren  15969  ausgrusgrben  15974  umgr2edg1  16015  usgredg2vlem1  16028  wlkvtxm  16061  g0wlk0  16091  wlkres  16098  trlreslem  16107  bj-stand  16136  bj-charfundcALT  16196  bj-charfunbi  16198  bj-bdfindis  16334  bj-peano4  16342  strcollnfALT  16373  1dom1el  16378  2omap  16388  pw1map  16390  pwtrufal  16392  pwf1oexmid  16394  subctctexmid  16395  pw1nct  16398  nnsf  16401  nninfalllem1  16404  nninfall  16405  nninfsellemqall  16411  nnnninfen  16417  exmidsbthrlem  16420  sbthom  16424  cvgcmp2nlemabs  16430  trilpo  16441  iswomni0  16449  redcwlpo  16453  dceqnconst  16458  dcapnconst  16459  nconstwlpolem  16463  nconstwlpo  16464  neapmkvlem  16465  neapmkv  16466  ltlenmkv  16468  taupi  16471  alsi1d  16479  alsi2d  16480  alsc1d  16481  alsc2d  16482