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  729  3mix3  1168  mpjao3dan  1307  ecase23d  1350  exlimdh  1596  nexd  1613  alexnim  1648  excomim  1663  19.41  1686  equcomd  1707  nfexd  1761  sbh  1776  sbcof2  1810  sbidm  1851  sb6rf  1853  nfsbt  1976  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  eu2  2070  2euex  2113  eqcomd  2183  3eltr3g  2262  abbid  2294  neneqd  2368  eqnetrrid  2378  3netr3g  2381  necomd  2433  r19.21bi  2565  nrexdv  2570  rexlimd  2591  rabbidva  2727  elisset  2753  euind  2926  rmoan  2939  reuind  2944  2rmorex  2945  spsbc  2976  spesbc  3050  eldifad  3142  eldifbd  3143  3sstr3g  3199  sseqtrdi  3205  difindiss  3391  un00  3471  undifss  3505  ifcldcd  3572  disjpr2  3658  difprsn1  3733  diftpsn3  3735  difsnss  3740  sneqr  3762  preqr1  3770  preq12b  3772  oprcl  3804  intab  3875  riinm  3961  rintm  3981  disjiun  4000  sndisj  4001  3brtr3g  4038  trint  4118  iinexgm  4156  exmidexmid  4198  exmid01  4200  pwntru  4201  exmid1stab  4210  pwel  4220  exss  4229  0nelop  4250  euotd  4256  opelopabsb  4262  pwunim  4288  issod  4321  frind  4354  suctr  4423  orduniss  4427  onelini  4432  oneluni  4433  eusv2i  4457  rexxfrd  4465  rabxfrd  4471  reuhypd  4473  iunpw  4482  sucexg  4499  ordsucim  4501  ordtriexmidlem  4520  ontriexmidim  4523  ordtri2or2exmidlem  4527  onsucelsucexmidlem  4530  ordsucunielexmid  4532  orddif  4548  suc11g  4558  onintexmid  4574  reg3exmidlemwe  4580  tfisi  4588  peano1  4595  peano2  4596  finds2  4602  omsinds  4623  brrelex12  4666  brel  4680  ssrel  4716  ssrel2  4718  ssrelrel  4728  elrel  4730  xpsspw  4740  relop  4779  dmxpm  4849  opelresi  4920  ndmima  5007  poirr2  5023  xpmlem  5051  xpimasn  5079  iotass  5197  iotacl  5203  dffun5r  5230  funeu  5243  funeu2  5244  funfnd  5249  funopg  5252  funun  5262  funinsn  5267  funtp  5271  funcnvuni  5287  funcnvres2  5293  imadiflem  5297  imadif  5298  funimaexglem  5301  fneu2  5323  fnimaeq0  5339  fnmpt  5344  fun2  5391  f00  5409  f0bi  5410  foimacnv  5481  resdif  5485  f1ococnv1  5492  fv3  5540  relelfvdm  5549  nfvres  5550  dffn5im  5563  mptfvex  5603  fvmptdf  5605  fvmptdv2  5607  fndmdif  5623  dff4im  5664  fmpt  5668  fmptd  5672  fmptdf  5675  f1oresrab  5683  fcoconst  5689  fsn  5690  ftpg  5702  fsnunf  5718  resfunexg  5739  isores1  5817  riota2df  5853  acexmidlemcase  5872  brabvv  5923  funoprabg  5976  fnovim  5985  ovmpodf  6008  ovi3  6013  elmpocl  6071  1stcof  6166  2ndcof  6167  fnmpo  6205  fmpoco  6219  fo2ndf  6230  f1o2ndf1  6231  disjxp1  6239  brtpos2  6254  reldmtpos  6256  dftpos3  6265  dftpos4  6266  tpostpos2  6268  tposf2  6271  tposf12  6272  tposfo  6274  tposf  6275  smores2  6297  tfrlem1  6311  tfrlem3-2d  6315  tfrlemisucaccv  6328  tfrlemibxssdm  6330  tfrlemibfn  6331  tfrlemi1  6335  tfrexlem  6337  tfr1onlemsucaccv  6344  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfr1onlemaccex  6351  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllembfn  6360  tfrcllemaccex  6364  tfrcldm  6366  rdgivallem  6384  rdgisucinc  6388  frecabex  6401  frecfnom  6404  frecfcllem  6407  frecsuclem  6409  omsuc  6475  nntri2  6497  nnsucuniel  6498  nnsseleq  6504  nnm00  6533  ecexr  6542  swoer  6565  elqsn0m  6605  iinerm  6609  erinxp  6611  ecinxp  6612  eroveu  6628  eroprf  6630  mapprc  6654  mapsn  6692  ixpprc  6721  ixp0  6733  resixp  6735  elixpsn  6737  dom2lem  6774  fundmen  6808  dom0  6840  xpf1o  6846  mapxpen  6850  xpmapenlem  6851  ssenen  6853  nneneq  6859  ssfilem  6877  dif1en  6881  dif1enen  6882  fin0  6887  fin0or  6888  diffitest  6889  diffisn  6895  ac6sfi  6900  fimax2gtrilemstep  6902  fimax2gtri  6903  finexdc  6904  exmidpweq  6911  pw1fin  6912  onunsnss  6918  unsnfidcel  6922  undifdcss  6924  undifdc  6925  fiintim  6930  fisseneq  6933  fidcenumlemr  6956  sbthlemi4  6961  sbthlemi5  6962  sbthlemi9  6966  fifo  6981  suplubti  7001  supelti  7003  infmoti  7029  infisoti  7033  djulclb  7056  updjud  7083  omp1eomlem  7095  0ct  7108  ctmlemr  7109  ctssdclemn0  7111  ctssdccl  7112  ctssdc  7114  enumct  7116  nnnninfeq2  7129  finomni  7140  fodjuomnilemdc  7144  fodjum  7146  fodjuomnilemres  7148  fodjumkvlemres  7159  omniwomnimkv  7167  nninfwlporlem  7173  nninfwlpoimlemginf  7176  nninfwlpoim  7178  exmidonfinlem  7194  en2eleq  7196  exmidfodomrlemeldju  7200  exmidfodomrlemreseldju  7201  exmidfodomrlemim  7202  acfun  7208  exmidaclem  7209  exmidontriimlem3  7224  exmidontriimlem4  7225  exmidontriim  7226  pw1on  7227  dftap2  7252  2omotaplemst  7259  exmidapne  7261  ccfunen  7265  cc1  7266  cc2lem  7267  cc2  7268  cc3  7269  elni2  7315  indpi  7343  distrnqg  7388  subhalfnqq  7415  enq0sym  7433  enq0ref  7434  enq0tr  7435  nqnq0pi  7439  nnnq0lem1  7447  distrnq0  7460  elinp  7475  elnp1st2nd  7477  prltlu  7488  prnmaxl  7489  prnminu  7490  prarloc  7504  nqprm  7543  appdivnq  7564  prmuloc  7567  mullocpr  7572  distrlem4prl  7585  distrlem4pru  7586  ltexprlemm  7601  ltexprlemopl  7602  ltexprlemopu  7604  cauappcvgprlemopl  7647  cauappcvgprlemopu  7649  cauappcvgprlemdisj  7652  cauappcvgprlem2  7661  cauappcvgprlemlim  7662  caucvgprlemnkj  7667  caucvgprlemopl  7670  caucvgprlemopu  7672  caucvgprlemdisj  7675  caucvgprlemcl  7677  caucvgprlemladdfu  7678  caucvgprlemladdrl  7679  caucvgprlem2  7681  caucvgprprlemcbv  7688  caucvgprprlemval  7689  caucvgprprlemlol  7699  caucvgprprlemexbt  7707  caucvgprprlem1  7710  suplocexprlemrl  7718  suplocexprlemmu  7719  suplocexprlemru  7720  suplocexprlemdisj  7721  suplocexprlemloc  7722  suplocexprlemub  7724  suplocexprlemlub  7725  prsrlem1  7743  gt0srpr  7749  caucvgsrlemcl  7790  caucvgsrlembound  7795  caucvgsrlemgt1  7796  suplocsrlemb  7807  suplocsrlem  7809  suplocsr  7810  ltresr  7840  nnindnn  7894  axcaucvglemcl  7896  axcaucvglemval  7898  axcaucvglemcau  7899  axcaucvglemres  7900  axpre-suploclemres  7902  axpre-suploc  7903  sup3exmid  8916  nnind  8937  nn0supp  9230  nn0ge2m1nn  9238  zleloe  9302  zapne  9329  nn0lt2  9336  suprzclex  9353  zindd  9373  uzm1  9560  uzin  9562  infregelbex  9600  elnn1uz2  9609  nn01to3  9619  divfnzn  9623  qapne  9641  xrltnsym2  9796  xaddass  9871  xleadd1a  9875  xlt2add  9882  xlesubadd  9885  iooval2  9917  icoshftf1o  9993  fztri3or  10041  fzneuz  10103  4fvwrd4  10142  elfzo0  10184  exbtwnzlemex  10252  ioom  10263  fzfig  10432  uzennn  10438  uzsinds  10444  iseqovex  10458  seq3val  10460  seqvalcd  10461  seqf  10463  seqovcd  10465  monoord2  10479  iseqf1olemjpcl  10497  iseqf1olemqpcl  10498  seq3f1olemqsum  10502  seq3f1o  10506  seq3distr  10515  expp1  10529  expcl2lemap  10534  expclzap  10547  expap0i  10554  nn0ltexp2  10691  bcval5  10745  hashinfuni  10759  hashennnuni  10761  hashnncl  10777  resunimafz0  10813  zfz1isolemiso  10821  zfz1isolem1  10822  zfz1iso  10823  seq3shft  10849  cvg1nlemcau  10995  rexanuz  10999  resqrexlemoverl  11032  resqrexlemglsq  11033  resqrexlemsqa  11035  resqrexlemex  11036  rersqreu  11039  caubnd2  11128  maxleast  11224  fimaxre2  11237  minmax  11240  xrmaxiflemcl  11255  xrmaxiflemab  11257  xrmaxiflemlub  11258  xrmaxadd  11271  xrminmax  11275  xrbdtri  11286  climreu  11307  reccn2ap  11323  iserex  11349  climcvg1nlem  11359  serf0  11362  fz1f1o  11385  summodclem3  11390  zsumdc  11394  fsum3  11397  isumz  11399  isumss  11401  isumss2  11403  fsumsersdc  11405  fsum3ser  11407  fsumsplit  11417  isumclim2  11432  isumclim3  11433  fsum2dlemstep  11444  fsumcnv  11447  fisumcom2  11448  bcxmas  11499  isumle  11505  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  cvgratz  11542  mertenslemub  11544  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  zproddc  11589  prod1dc  11596  fprodsplitdc  11606  fprodsplit  11607  fprodunsn  11614  fprodcl2lem  11615  fprodcllemf  11623  fprod2dlemstep  11632  fprodcnv  11635  fprodcom2fi  11636  fprodle  11650  ef0lem  11670  mod2eq1n2dvds  11886  ndvdssub  11937  infssuzex  11952  infssuzcldc  11954  suprzubdc  11955  nninfdcex  11956  zsupssdc  11957  gcdsupex  11960  gcdsupcl  11961  bezoutlemnewy  11999  bezoutlemmain  12001  bezoutlembi  12008  bezoutlemeu  12010  bezoutlemle  12011  uzwodc  12040  nnwofdc  12041  nnwosdc  12042  nn0seqcvgd  12043  eucalgf  12057  eucalginv  12058  lcmval  12065  prmind2  12122  dfphi2  12222  phiprmpw  12224  phimullem  12227  eulerthlem1  12229  eulerthlemrprm  12231  eulerthlema  12232  eulerthlemh  12233  eulerthlemth  12234  eulerth  12235  phisum  12242  odzcllem  12244  odzdvds  12247  pythagtriplem19  12284  pclemub  12289  pcprecl  12291  pceu  12297  pcqmul  12305  pcqcl  12308  pcxnn0cl  12312  pcge0  12314  pcdvdsb  12321  pceq0  12323  pcneg  12326  pcdvdstr  12328  pcgcd1  12329  pc2dvds  12331  pcz  12333  pcprmpw2  12334  pcaddlem  12340  pcadd  12341  pcmptcl  12342  pcmpt  12343  pcmptdvds  12345  fldivp1  12348  qexpz  12352  pockthlem  12356  pockthg  12357  prmunb  12362  1arith  12367  ennnfonelemom  12411  ennnfoneleminc  12414  ennnfonelemhf1o  12416  ennnfonelemex  12417  ennnfonelemhom  12418  ennnfonelemdm  12423  ennnfonelemr  12426  ennnfonelemim  12427  exmidunben  12429  ctinfom  12431  inffinp1  12432  ctinf  12433  enctlem  12435  ctiunctlemu1st  12437  ctiunctlemu2nd  12438  ctiunctlemudc  12440  ctiunct  12443  ctiunctal  12444  unct  12445  ssomct  12448  nninfdclemcl  12451  nninfdclemp1  12453  nninfdc  12456  structcnvcnv  12480  setscom  12504  ressbas2d  12530  ressval3d  12533  ressabsg  12537  restid2  12702  imasaddfnlemg  12740  quslem  12750  ercpbl  12755  fnpr2ob  12764  mgmplusf  12790  grprinvlem  12809  grprinvd  12810  grpridd  12811  ismnd  12825  mhmpropd  12862  grppropd  12898  grpsubf  12954  dfgrp3mlem  12973  mulgnn0p1  12999  mulgnn0subcl  13001  mulgsubcl  13002  mulgneg  13006  mulgnn0dir  13018  mulgnn0ass  13024  issubg2m  13054  issubg4m  13058  lringuplu  13342  lmodscaf  13405  lssintclm  13476  topontopon  13559  eltg3i  13595  epttop  13629  difopn  13647  uncld  13652  0nnei  13692  resttopon  13710  restabs  13714  restopnb  13720  lmcvg  13756  cnptopco  13761  cnss1  13765  cnss2  13766  cncnpi  13767  cncnp2m  13770  cnrest  13774  cnrest2  13775  cnrest2r  13776  cnptoprest  13778  cnptoprest2  13779  lmss  13785  lmff  13788  lmtopcnp  13789  lmcn  13790  txbasval  13806  upxp  13811  txcnmpt  13812  txdis1cn  13817  txlm  13818  lmcn2  13819  cnmpt11  13822  cnmpt11f  13823  cnmpt1t  13824  cnmpt12  13826  cnmpt21  13830  cnmpt21f  13831  cnmpt2t  13832  cnmpt22  13833  cnmpt22f  13834  cnmptcom  13837  hmeocnv  13846  hmeof1o  13848  hmeores  13854  txhmeo  13858  txswaphmeo  13860  isxmet2d  13887  blfvalps  13924  xblss2ps  13943  xblss2  13944  blfps  13948  blf  13949  unirnblps  13961  unirnbl  13962  isxms2  13991  bdxmet  14040  bdmet  14041  xmetxp  14046  xmettx  14049  blssioo  14084  tgioo  14085  mulcncflem  14129  dedekindeulemuub  14134  dedekindeulemub  14135  dedekindeulemloc  14136  dedekindeulemlu  14138  suplociccreex  14141  suplociccex  14142  dedekindicclemuub  14143  dedekindicclemub  14144  dedekindicclemloc  14145  dedekindicclemlu  14147  dedekindicc  14150  ivthinclemlopn  14153  ivthinclemuopn  14155  limcrcl  14166  limcmpted  14171  limccnp2lem  14184  limccnp2cntop  14185  limccoap  14186  dvrecap  14216  cosordlem  14309  logbgcd1irraplemexp  14425  logbgcd1irrap  14427  lgsneg1  14465  lgsdilem  14467  lgsdir2  14473  lgsdirprm  14474  lgsdir  14475  lgsne0  14478  lgsabs1  14479  lgsdirnn0  14487  lgsdinn0  14488  lgseisenlem1  14489  2sqlem5  14505  2sqlem7  14507  2sqlem8a  14508  2sqlem8  14509  2sqlem9  14510  bj-stand  14539  bj-charfundcALT  14600  bj-charfunbi  14602  bj-bdfindis  14738  bj-peano4  14746  strcollnfALT  14777  pwtrufal  14786  pwf1oexmid  14788  subctctexmid  14789  pw1nct  14791  nnsf  14793  nninfalllem1  14796  nninfall  14797  nninfsellemqall  14803  exmidsbthrlem  14809  sbthom  14813  cvgcmp2nlemabs  14819  trilpo  14830  iswomni0  14838  redcwlpo  14842  dceqnconst  14846  dcapnconst  14847  nconstwlpolem  14851  nconstwlpo  14852  neapmkvlem  14853  neapmkv  14854  ltlenmkv  14856  taupi  14859  alsi1d  14867  alsi2d  14868  alsc1d  14869  alsc2d  14870