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  2030  dvelimALT  2064  dvelimfv  2065  dvelimor  2072  eu2  2125  2euex  2168  eqcomd  2238  3eltr3g  2317  abbid  2349  neneqd  2433  eqnetrrid  2443  3netr3g  2446  necomd  2498  r19.21bi  2630  nrexdv  2635  rexlimd  2657  rabbidva  2800  elisset  2827  euind  3003  rmoan  3016  reuind  3021  2rmorex  3022  spsbc  3053  spesbc  3128  eldifad  3221  eldifbd  3222  3sstr3g  3279  sseqtrdi  3285  difindiss  3474  un00  3554  undifss  3589  ifcldcd  3659  disjpr2  3752  difprsn1  3832  diftpsn3  3834  difsnss  3839  sneqr  3863  preqr1  3871  preq12b  3873  oprcl  3906  intab  3977  riinm  4063  rintm  4083  disjiun  4103  sndisj  4104  3brtr3g  4141  trint  4222  iinexgm  4265  exmidexmid  4308  exmid01  4310  pwntru  4311  exmid1stab  4320  pwel  4333  exss  4342  0nelop  4363  euotd  4370  opelopabsb  4377  pwunim  4406  issod  4439  frind  4472  suctr  4541  orduniss  4545  onelini  4550  oneluni  4551  eusv2i  4575  rexxfrd  4583  rabxfrd  4589  reuhypd  4591  iunpw  4600  sucexg  4619  ordsucim  4621  ordtriexmidlem  4640  ontriexmidim  4643  ordtri2or2exmidlem  4647  onsucelsucexmidlem  4650  ordsucunielexmid  4652  orddif  4668  suc11g  4678  onintexmid  4694  reg3exmidlemwe  4700  tfisi  4708  peano1  4715  peano2  4716  finds2  4722  omsinds  4743  brrelex12  4787  brel  4801  ssrel  4837  ssrel2  4839  ssrelrel  4849  elrel  4851  xpsspw  4861  relop  4904  dmxpm  4976  opelresi  5048  mptimass  5113  ndmima  5138  poirr2  5154  xpmlem  5182  xpimasn  5210  iotass  5329  iotacl  5336  dffun5r  5363  funeu  5376  funeu2  5377  funfnd  5382  funopg  5385  funun  5396  fununfun  5398  funinsn  5404  funtp  5408  funcnvuni  5424  funcnvres2  5430  imadiflem  5434  imadif  5435  funimaexglem  5438  fneu2  5462  fnimaeq0  5479  fnmpt  5484  ffrn  5519  fun2  5536  f00  5558  f0bi  5559  fimadmfo  5598  foimacnv  5631  resdif  5635  f1ococnv1  5642  fv3  5692  relelfvdm  5701  elfvm  5702  nfvres  5705  dffn5im  5721  mptfvex  5762  fvmptdf  5764  fvmptdv2  5766  fndmdif  5782  dff4im  5822  fmpt  5826  fmptd  5830  fmptdf  5833  f1oresrab  5841  fcoconst  5847  fsn  5848  funopsn  5859  ftpg  5867  fsnunf  5883  resfunexg  5904  isores1  5986  riota2df  6024  acexmidlemcase  6044  brabvv  6098  funoprabg  6151  fnovim  6161  ovmpodf  6184  ovi3  6190  elmpocl  6248  uchoice  6330  1stcof  6356  2ndcof  6357  opabn1stprc  6388  fnmpo  6397  fmpoco  6411  fo2ndf  6422  f1o2ndf1  6423  disjxp1  6431  fvdifsuppst  6443  fsuppeq  6446  fsuppeqg  6447  suppssrst  6460  suppssrgst  6461  brtpos2  6481  reldmtpos  6483  dftpos3  6492  dftpos4  6493  tpostpos2  6495  tposf2  6498  tposf12  6499  tposfo  6501  tposf  6502  smores2  6524  tfrlem1  6538  tfrlem3-2d  6542  tfrlemisucaccv  6555  tfrlemibxssdm  6557  tfrlemibfn  6558  tfrlemi1  6562  tfrexlem  6564  tfr1onlemsucaccv  6571  tfr1onlembxssdm  6573  tfr1onlembfn  6574  tfr1onlemaccex  6578  tfrcllemsucaccv  6584  tfrcllembxssdm  6586  tfrcllembfn  6587  tfrcllemaccex  6591  tfrcldm  6593  rdgivallem  6611  rdgisucinc  6615  frecabex  6628  frecfnom  6631  frecfcllem  6634  frecsuclem  6636  omsuc  6704  nntri2  6726  nnsucuniel  6727  nnsseleq  6733  nnm00  6762  ecexr  6771  swoer  6794  elqsn0m  6836  iinerm  6840  erinxp  6842  ecinxp  6843  eroveu  6859  eroprf  6861  mapprc  6885  mapsn  6924  ixpprc  6953  ixp0  6965  resixp  6967  elixpsn  6969  dom2lem  7010  fundmen  7046  1dom1el  7059  dom0  7090  xpf1o  7096  mapxpen  7100  xpmapenlem  7101  ssenen  7104  nneneq  7110  ssfilem  7129  ssfilemd  7131  dif1en  7135  dif1enen  7136  fin0  7141  fin0or  7142  diffitest  7143  diffisn  7149  ac6sfi  7154  fimax2gtrilemstep  7157  fimax2gtri  7158  finexdc  7159  eqsndc  7162  exmidpweq  7168  pw1fin  7169  onunsnss  7176  unsnfidcel  7180  undifdcss  7182  undifdc  7183  tpfidceq  7189  fiintim  7190  fisseneq  7194  fidcenumlemr  7224  sbthlemi4  7229  sbthlemi5  7230  sbthlemi9  7234  fifo  7266  2omap  7268  suplubti  7290  supelti  7292  infmoti  7318  infisoti  7322  djulclb  7345  updjud  7372  omp1eomlem  7384  0ct  7397  ctmlemr  7398  ctssdclemn0  7400  ctssdccl  7401  ctssdc  7403  enumct  7405  nninfninc  7413  nnnninfeq2  7419  finomni  7430  fodjuomnilemdc  7434  fodjum  7436  fodjuomnilemres  7438  fodjumkvlemres  7449  omniwomnimkv  7457  nninfwlporlem  7463  nninfwlpoimlemginf  7466  nninfwlpoim  7469  nninfinfwlpo  7470  ficardon  7484  pr2cv1  7491  exmidonfinlem  7495  en2eleq  7497  exmidfodomrlemeldju  7501  exmidfodomrlemreseldju  7502  exmidfodomrlemim  7503  finacn  7510  acfun  7513  exmidaclem  7514  exmidontriimlem3  7529  exmidontriimlem4  7530  exmidontriim  7531  pw1if  7534  pw1on  7535  papsym  7560  papcotr  7561  dftap2  7564  2omotaplemst  7571  exmidapne  7573  ccfunen  7577  cc1  7578  cc2lem  7579  cc2  7580  cc3  7581  acnccim  7585  elni2  7628  indpi  7656  distrnqg  7701  subhalfnqq  7728  enq0sym  7746  enq0ref  7747  enq0tr  7748  nqnq0pi  7752  nnnq0lem1  7760  distrnq0  7773  elinp  7788  elnp1st2nd  7790  prltlu  7801  prnmaxl  7802  prnminu  7803  prarloc  7817  nqprm  7856  appdivnq  7877  prmuloc  7880  mullocpr  7885  distrlem4prl  7898  distrlem4pru  7899  ltexprlemm  7914  ltexprlemopl  7915  ltexprlemopu  7917  cauappcvgprlemopl  7960  cauappcvgprlemopu  7962  cauappcvgprlemdisj  7965  cauappcvgprlem2  7974  cauappcvgprlemlim  7975  caucvgprlemnkj  7980  caucvgprlemopl  7983  caucvgprlemopu  7985  caucvgprlemdisj  7988  caucvgprlemcl  7990  caucvgprlemladdfu  7991  caucvgprlemladdrl  7992  caucvgprlem2  7994  caucvgprprlemcbv  8001  caucvgprprlemval  8002  caucvgprprlemlol  8012  caucvgprprlemexbt  8020  caucvgprprlem1  8023  suplocexprlemrl  8031  suplocexprlemmu  8032  suplocexprlemru  8033  suplocexprlemdisj  8034  suplocexprlemloc  8035  suplocexprlemub  8037  suplocexprlemlub  8038  prsrlem1  8056  gt0srpr  8062  caucvgsrlemcl  8103  caucvgsrlembound  8108  caucvgsrlemgt1  8109  suplocsrlemb  8120  suplocsrlem  8122  suplocsr  8123  ltresr  8153  nnindnn  8207  axcaucvglemcl  8209  axcaucvglemval  8211  axcaucvglemcau  8212  axcaucvglemres  8213  axpre-suploclemres  8215  axpre-suploc  8216  sup3exmid  9230  nnind  9252  nn0supp  9551  nn0ge2m1nn  9559  zleloe  9623  zapne  9651  nn0lt2  9658  suprzclex  9675  zindd  9695  uzm1  9884  uzin  9886  infregelbex  9929  elnn1uz2  9938  nn01to3  9948  divfnzn  9952  qapne  9970  xrltnsym2  10126  xaddass  10201  xleadd1a  10205  xlt2add  10212  xlesubadd  10215  iooval2  10247  icoshftf1o  10323  fztri3or  10372  fzneuz  10434  4fvwrd4  10473  elfzo0  10519  infssuzex  10592  infssuzcldc  10594  suprzubdc  10595  nninfdcex  10596  zsupssdc  10597  exbtwnzlemex  10608  ioom  10619  fzfig  10791  uzennn  10797  uzsinds  10805  iseqovex  10819  seq3val  10821  seqvalcd  10822  seqf  10825  seqovcd  10828  monoord2  10847  iseqf1olemjpcl  10869  iseqf1olemqpcl  10870  seq3f1olemqsum  10874  seq3f1o  10878  seqf1og  10882  seq3distr  10893  expp1  10907  expcl2lemap  10912  expclzap  10925  expap0i  10932  nn0ltexp2  11070  bcval5  11124  hashinfuni  11138  hashennnuni  11140  hashnncl  11156  resunimafz0  11194  zfz1isolemiso  11207  zfz1isolem1  11208  zfz1iso  11209  wrdsymb0  11253  wrdlen1  11258  ccat1st1st  11325  swrdrlen  11349  pfxid  11374  pfxwrdsymbg  11378  pfxtrcfv  11381  pfxccat1  11390  pfxpfxid  11397  pfxcctswrd  11398  swrdccatin1  11413  pfxccatin12  11421  pfxccatid  11429  seq3shft  11519  cvg1nlemcau  11665  rexanuz  11669  resqrexlemoverl  11702  resqrexlemglsq  11703  resqrexlemsqa  11705  resqrexlemex  11706  rersqreu  11709  caubnd2  11798  maxleast  11894  fimaxre2  11908  minmax  11911  xrmaxiflemcl  11926  xrmaxiflemab  11928  xrmaxiflemlub  11929  xrmaxadd  11942  xrminmax  11946  xrbdtri  11957  climreu  11978  reccn2ap  11994  iserex  12020  climcvg1nlem  12030  serf0  12033  fz1f1o  12056  summodclem3  12062  zsumdc  12066  fsum3  12069  isumz  12071  isumss  12073  isumss2  12075  fsumsersdc  12077  fsum3ser  12079  fsumsplit  12089  isumclim2  12104  isumclim3  12105  fsum2dlemstep  12116  fsumcnv  12119  fisumcom2  12120  bcxmas  12171  isumle  12177  cvgratnnlemnexp  12206  cvgratnnlemmn  12207  cvgratz  12214  mertenslemub  12216  mertenslemi1  12217  mertenslem2  12218  mertensabs  12219  zproddc  12261  prod1dc  12268  fprodsplitdc  12278  fprodsplit  12279  fprodunsn  12286  fprodcl2lem  12287  fprodcllemf  12295  fprod2dlemstep  12304  fprodcnv  12307  fprodcom2fi  12308  fprodle  12322  ef0lem  12342  fsumdvds  12524  mod2eq1n2dvds  12561  ndvdssub  12612  bitsfzolem  12636  bitsfzo  12637  bitsinv1  12644  gcdsupex  12649  gcdsupcl  12650  bezoutlemnewy  12688  bezoutlemmain  12690  bezoutlembi  12697  bezoutlemeu  12699  bezoutlemle  12700  uzwodc  12729  nnwofdc  12730  nnwosdc  12731  nninfctlemfo  12732  nninfct  12733  nn0seqcvgd  12734  eucalgf  12748  eucalginv  12749  lcmval  12756  prmind2  12813  dfphi2  12913  phiprmpw  12915  phimullem  12918  eulerthlem1  12920  eulerthlemrprm  12922  eulerthlema  12923  eulerthlemh  12924  eulerthlemth  12925  eulerth  12926  phisum  12934  odzcllem  12936  odzdvds  12939  pythagtriplem19  12976  pclemub  12981  pcprecl  12983  pceu  12989  pcqmul  12997  pcqcl  13000  pcxnn0cl  13004  pcxqcl  13006  pcge0  13007  pcdvdsb  13014  pceq0  13016  pcneg  13019  pcdvdstr  13021  pcgcd1  13022  pc2dvds  13024  pcz  13026  pcprmpw2  13027  pcaddlem  13033  pcadd  13034  pcmptcl  13036  pcmpt  13037  pcmptdvds  13039  fldivp1  13042  qexpz  13046  pockthlem  13050  pockthg  13051  prmunb  13056  1arith  13061  4sqlemffi  13090  4sqlem17  13101  4sqlem18  13102  4sqlem19  13103  ennnfonelemom  13151  ennnfoneleminc  13154  ennnfonelemhf1o  13156  ennnfonelemex  13157  ennnfonelemhom  13158  ennnfonelemdm  13163  ennnfonelemr  13166  ennnfonelemim  13167  exmidunben  13169  ctinfom  13171  inffinp1  13172  ctinf  13173  enctlem  13175  ctiunctlemu1st  13177  ctiunctlemu2nd  13178  ctiunctlemudc  13180  ctiunct  13183  ctiunctal  13184  unct  13185  ssomct  13188  nninfdclemcl  13191  nninfdclemp1  13193  nninfdc  13196  structcnvcnv  13220  setscom  13244  relelbasov  13267  ressbas2d  13273  ressval3d  13277  ressabsg  13281  restid2  13453  imasaddfnlemg  13519  quslem  13529  ercpbl  13536  fnpr2ob  13545  mgmplusf  13571  grpinvalem  13590  grpinva  13591  grprida  13592  fngsum  13593  igsumvalx  13594  gsum0g  13601  gsumval2  13602  ismnd  13624  mhmpropd  13671  grppropd  13722  grpsubf  13784  dfgrp3mlem  13803  mulgnn0p1  13842  mulgnn0subcl  13844  mulgsubcl  13845  mulgneg  13849  mulgnn0dir  13861  mulgnn0ass  13867  submmulg  13875  issubg2m  13898  issubg4m  13902  ghmmulg  13965  ghmrn  13966  lringuplu  14333  rrgsupp  14403  lmodscaf  14450  lssintclm  14524  lspun0  14565  lidlbas  14618  psrbagconcl  14819  psr1clfi  14835  topontopon  14877  eltg3i  14913  epttop  14947  difopn  14965  uncld  14970  0nnei  15010  resttopon  15028  restabs  15032  restopnb  15038  lmcvg  15074  cnptopco  15079  cnss1  15083  cnss2  15084  cncnpi  15085  cncnp2m  15088  cnrest  15092  cnrest2  15093  cnrest2r  15094  cnptoprest  15096  cnptoprest2  15097  lmss  15103  lmff  15106  lmtopcnp  15107  lmcn  15108  txbasval  15124  upxp  15129  txcnmpt  15130  txdis1cn  15135  txlm  15136  lmcn2  15137  cnmpt11  15140  cnmpt11f  15141  cnmpt1t  15142  cnmpt12  15144  cnmpt21  15148  cnmpt21f  15149  cnmpt2t  15150  cnmpt22  15151  cnmpt22f  15152  cnmptcom  15155  hmeocnv  15164  hmeof1o  15166  hmeores  15172  txhmeo  15176  txswaphmeo  15178  isxmet2d  15205  blfvalps  15242  xblss2ps  15261  xblss2  15262  blfps  15266  blf  15267  unirnblps  15279  unirnbl  15280  isxms2  15309  bdxmet  15358  bdmet  15359  xmetxp  15364  xmettx  15367  blssioo  15410  tgioo  15411  mulcncflem  15464  divcncfap  15471  dedekindeulemuub  15474  dedekindeulemub  15475  dedekindeulemloc  15476  dedekindeulemlu  15478  suplociccreex  15481  suplociccex  15482  dedekindicclemuub  15483  dedekindicclemub  15484  dedekindicclemloc  15485  dedekindicclemlu  15487  dedekindicc  15490  ivthinclemlopn  15493  ivthinclemuopn  15495  ivthdich  15510  limcrcl  15515  limcmpted  15520  limccnp2lem  15533  limccnp2cntop  15534  limccoap  15535  dvrecap  15570  plyaddlem1  15604  plymullem1  15605  plycoeid3  15614  plyco  15616  plycj  15618  plyrecj  15620  dvply1  15622  dvply2g  15623  cosordlem  15706  logbgcd1irraplemexp  15825  logbgcd1irrap  15827  lgsneg1  15890  lgsdilem  15892  lgsdir2  15898  lgsdirprm  15899  lgsdir  15900  lgsne0  15903  lgsabs1  15904  lgsdirnn0  15912  lgsdinn0  15913  gausslemma2dlem1f1o  15925  gausslemma2dlem4  15929  lgseisenlem1  15935  lgsquadlem3  15944  2lgslem1a  15953  2sqlem5  15984  2sqlem7  15986  2sqlem8a  15987  2sqlem8  15988  2sqlem9  15989  gropeld  16036  grstructeld2dom  16037  uhgrm  16065  upgrm  16087  upgr1een  16111  uhgredgm  16123  edgupgren  16128  edgumgren  16129  edgusgren  16150  ausgrusgrben  16155  umgr2edg1  16196  usgredg2vlem1  16209  uhgr0enedgfi  16223  subupgr  16260  vtxedgfi  16276  vtxlpfi  16277  vtxdumgrfival  16285  vtxd0nedgbfi  16286  1hevtxdg0fi  16294  p1evtxdeqfilem  16298  wlkvtxm  16327  g0wlk0  16357  wlkres  16366  trlreslem  16376  clwwlkccatlem  16387  clwwlknnn  16399  trlsegvdeglem6  16452  eupth2lem3lem3fi  16457  eupth2lem3lem7fi  16461  eulerpathum  16468  bj-stand  16512  bj-charfundcALT  16571  bj-charfunbi  16573  bj-bdfindis  16709  bj-peano4  16717  strcollnfALT  16748  pw1map  16761  pwtrufal  16763  pwf1oexmid  16765  subctctexmid  16766  pw1nct  16769  nnsf  16775  nninfalllem1  16778  nninfall  16779  nninfsellemqall  16785  nnnninfen  16791  exmidsbthrlem  16794  sbthom  16798  repiecef  16804  cvgcmp2nlemabs  16808  trilpo  16819  iswomni0  16828  redcwlpo  16832  dceqnconst  16837  dcapnconst  16838  nconstwlpolem  16842  nconstwlpo  16843  neapmkvlem  16844  neapmkv  16845  ltlenmkv  16847  taupi  16850  gfsumval  16853  gsumgfsum  16857  alsi1d  16869  alsi2d  16870  alsc1d  16871  alsc2d  16872