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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylbb1  137  bicomd  141  pm5.74d  182  bitri  184  3imtr3i  200  ancomd  267  pm4.71d  397  pm4.71rd  398  imdistand  451  orcomd  741  3mix3  1199  mpjao3dan  1348  ecase23d  1391  exlimdh  1649  nexd  1666  alexnim  1701  excomim  1715  19.41  1738  equcomd  1759  nfexd  1814  sbh  1829  sbcof2  1863  sbidm  1904  sb6rf  1906  nfsbt  2036  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  eu2  2131  2euex  2174  eqcomd  2244  3eltr3g  2323  abbid  2355  neneqd  2441  eqnetrrid  2451  3netr3g  2454  necomd  2506  r19.21bi  2638  nrexdv  2643  rexlimd  2665  rabbidva  2809  elisset  2836  euind  3013  rmoan  3026  reuind  3031  2rmorex  3032  spsbc  3063  spesbc  3138  eldifad  3231  eldifbd  3232  3sstr3g  3290  sseqtrdi  3296  difindiss  3485  un00  3567  vvin  3569  undifss  3608  ifcldcd  3678  disjpr2  3773  difprsn1  3854  diftpsn3  3856  difsnss  3861  sneqr  3885  preqr1  3893  preq12b  3895  oprcl  3928  intab  3999  riinm  4085  rintm  4105  disjiun  4125  sndisj  4126  sn0disj  4127  3brtr3g  4164  trint  4246  iinexgm  4292  exmidexmid  4335  exmid01  4337  pwntru  4338  exmid1stab  4347  pwel  4360  exss  4369  0nelop  4390  euotd  4397  opelopabsb  4404  pwunim  4433  issod  4466  frind  4499  suctr  4568  orduniss  4572  onelini  4577  oneluni  4578  eusv2i  4603  rexxfrd  4611  rabxfrd  4617  reuhypd  4619  iunpw  4628  sucexg  4647  ordsucim  4649  ordtriexmidlem  4668  ontriexmidim  4671  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  ordsucunielexmid  4680  orddif  4696  suc11g  4706  onintexmid  4722  reg3exmidlemwe  4728  tfisi  4736  peano1  4743  peano2  4744  finds2  4750  omsinds  4771  brrelex12  4815  brel  4829  ssrel  4865  ssrel2  4867  ssrelrel  4877  elrel  4879  xpsspw  4889  relop  4932  dmxpm  5004  opelresi  5076  mptimass  5142  ndmima  5167  poirr2  5183  xpmlem  5211  xpimasn  5239  iotass  5358  iotacl  5365  dffun5r  5392  funeu  5405  funeu2  5406  funfnd  5411  funopg  5414  funun  5425  fununfun  5427  funinsn  5433  funtp  5437  funcnvuni  5453  funcnvres2  5459  imadiflem  5463  imadif  5464  funimaexglem  5467  fneu2  5491  fnimaeq0  5508  fnmpt  5513  ffrn  5548  fun2  5565  f00  5587  f0bi  5588  fimadmfo  5627  foimacnv  5660  resdif  5664  f1ococnv1  5671  fv3  5721  relelfvdm  5730  elfvm  5732  nfvres  5735  dffn5im  5751  mptfvex  5794  fvmptdf  5796  fvmptdv2  5798  fndmdif  5817  dff4im  5857  fmpt  5861  fmptd  5865  fmptdf  5868  f1oresrab  5876  fcoconst  5882  fsn  5883  funopsn  5894  ftpg  5902  fsnunf  5918  resfunexg  5939  mptmex  5948  isores1  6023  riota2df  6063  acexmidlemcase  6083  brabvv  6137  funoprabg  6190  fnovim  6200  ovmpodf  6223  ovi3  6229  elmpocl  6287  uchoice  6375  1stcof  6401  2ndcof  6402  opabn1stprc  6433  fnmpo  6442  fmpoco  6456  fo2ndf  6467  f1o2ndf1  6468  disjxp1  6476  fvdifsuppst  6488  fsuppeq  6491  fsuppeqg  6492  suppssrst  6505  suppssrgst  6506  brtpos2  6526  reldmtpos  6528  dftpos3  6537  dftpos4  6538  tpostpos2  6540  tposf2  6543  tposf12  6544  tposfo  6546  tposf  6547  smores2  6569  tfrlem1  6583  tfrlem3-2d  6587  tfrlemisucaccv  6600  tfrlemibxssdm  6602  tfrlemibfn  6603  tfrlemi1  6607  tfrexlem  6609  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemaccex  6623  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemaccex  6636  tfrcldm  6638  rdgivallem  6656  rdgisucinc  6660  frecabex  6673  frecfnom  6676  frecfcllem  6679  frecsuclem  6681  omsuc  6749  nntri2  6771  nnsucuniel  6772  nnsseleq  6778  nnm00  6807  ecexr  6816  swoer  6839  elqsn0m  6881  iinerm  6885  erinxp  6887  ecinxp  6888  eroveu  6904  eroprf  6906  mapprc  6930  mapsn  6977  ixpprc  7006  ixp0  7018  resixp  7020  elixpsn  7022  dom2lem  7063  fundmen  7099  1dom1el  7112  dom0  7143  xpf1o  7149  mapxpen  7153  xpmapenlem  7154  ssenen  7157  nneneq  7163  ssfilem  7182  ssfilemd  7184  dif1en  7188  dif1enen  7189  fin0  7194  fin0or  7195  diffitest  7196  diffisn  7202  ac6sfi  7207  fimax2gtrilemstep  7210  fimax2gtri  7211  finexdc  7212  eqsndc  7215  exmidpweq  7221  pw1fin  7222  onunsnss  7229  unsnfidcel  7233  undifdcss  7235  undifdc  7236  tpfidceq  7242  fiintim  7243  fisseneq  7247  fidcenumlemr  7278  sbthlemi4  7283  sbthlemi5  7284  sbthlemi9  7288  fifo  7320  2omap  7325  suplubti  7347  supelti  7349  infmoti  7375  infisoti  7379  djulclb  7402  updjud  7429  omp1eomlem  7441  0ct  7454  ctmlemr  7455  ctssdclemn0  7457  ctssdccl  7458  ctssdc  7460  enumct  7462  nninfninc  7470  nnnninfeq2  7476  finomni  7487  fodjuomnilemdc  7491  fodjum  7493  fodjuomnilemres  7495  fodjumkvlemres  7506  omniwomnimkv  7514  nninfwlporlem  7520  nninfwlpoimlemginf  7523  nninfwlpoim  7526  nninfinfwlpo  7527  ficardon  7541  pr2cv1  7548  exmidonfinlem  7552  en2eleq  7554  exmidfodomrlemeldju  7558  exmidfodomrlemreseldju  7559  exmidfodomrlemim  7560  finacn  7567  acfun  7570  exmidaclem  7571  exmidontriimlem3  7586  exmidontriimlem4  7587  exmidontriim  7588  pw1if  7591  pw1on  7592  papsym  7619  papcotr  7620  dftap2  7624  2omotaplemst  7631  exmidapne  7633  ccfunen  7637  cc1  7638  cc2lem  7639  cc2  7640  cc3  7641  acnccim  7645  elni2  7688  indpi  7716  distrnqg  7761  subhalfnqq  7788  enq0sym  7806  enq0ref  7807  enq0tr  7808  nqnq0pi  7812  nnnq0lem1  7820  distrnq0  7833  elinp  7848  elnp1st2nd  7850  prltlu  7861  prnmaxl  7862  prnminu  7863  prarloc  7877  nqprm  7916  appdivnq  7937  prmuloc  7940  mullocpr  7945  distrlem4prl  7958  distrlem4pru  7959  ltexprlemm  7974  ltexprlemopl  7975  ltexprlemopu  7977  cauappcvgprlemopl  8020  cauappcvgprlemopu  8022  cauappcvgprlemdisj  8025  cauappcvgprlem2  8034  cauappcvgprlemlim  8035  caucvgprlemnkj  8040  caucvgprlemopl  8043  caucvgprlemopu  8045  caucvgprlemdisj  8048  caucvgprlemcl  8050  caucvgprlemladdfu  8051  caucvgprlemladdrl  8052  caucvgprlem2  8054  caucvgprprlemcbv  8061  caucvgprprlemval  8062  caucvgprprlemlol  8072  caucvgprprlemexbt  8080  caucvgprprlem1  8083  suplocexprlemrl  8091  suplocexprlemmu  8092  suplocexprlemru  8093  suplocexprlemdisj  8094  suplocexprlemloc  8095  suplocexprlemub  8097  suplocexprlemlub  8098  prsrlem1  8116  gt0srpr  8122  caucvgsrlemcl  8163  caucvgsrlembound  8168  caucvgsrlemgt1  8169  suplocsrlemb  8180  suplocsrlem  8182  suplocsr  8183  ltresr  8213  nnindnn  8267  axcaucvglemcl  8269  axcaucvglemval  8271  axcaucvglemcau  8272  axcaucvglemres  8273  axpre-suploclemres  8275  axpre-suploc  8276  sup3exmid  9296  indconst0  9312  indconst1  9313  nnind  9330  nn0supp  9631  nn0ge2m1nn  9639  zleloe  9703  zapne  9731  nn0lt2  9739  suprzclex  9756  zindd  9776  uzm1  9970  uzin  9972  infregelbex  10015  elnn1uz2  10024  nn01to3  10034  divfnzn  10038  qapne  10056  irraddap  10064  xrltnsym2  10214  xaddass  10289  xleadd1a  10293  xlt2add  10300  xlesubadd  10303  iooval2  10335  icoshftf1o  10411  fztri3or  10461  fzneuz  10526  4fvwrd4  10565  elfzo0  10611  infssuzex  10684  infssuzcldc  10686  infssfzcldc  10687  infssfzledc  10688  suprzubdc  10689  nninfdcex  10690  zsupssdc  10691  exbtwnzlemex  10702  ioom  10713  fzfig  10889  uzennn  10895  uzsinds  10903  iseqovex  10917  seq3val  10919  seqvalcd  10920  seqf  10923  seqovcd  10926  monoord2  10945  iseqf1olemjpcl  10967  iseqf1olemqpcl  10968  seq3f1olemqsum  10972  seq3f1o  10976  seqf1og  10980  seq3distr  10991  expp1  11005  expcl2lemap  11010  expclzap  11023  expap0i  11030  nn0ltexp2  11170  bcval5  11224  hashinfuni  11239  hashennnuni  11241  hashnncl  11257  resunimafz0  11297  hashf1lem2  11309  hashf1  11310  zfz1isolemiso  11314  zfz1isolem1  11315  zfz1iso  11316  wrdsymb0  11360  wrdlen1  11365  ccat1st1st  11432  swrdrlen  11456  pfxid  11481  pfxwrdsymbg  11485  pfxtrcfv  11488  pfxccat1  11497  pfxpfxid  11504  pfxcctswrd  11505  swrdccatin1  11520  pfxccatin12  11528  pfxccatid  11536  seq3shft  11626  cvg1nlemcau  11773  rexanuz  11777  resqrexlemoverl  11810  resqrexlemglsq  11811  resqrexlemsqa  11813  resqrexlemex  11814  rersqreu  11817  caubnd2  11907  maxleast  12003  fimaxre2  12017  minmax  12021  xrmaxiflemcl  12037  xrmaxiflemab  12039  xrmaxiflemlub  12040  xrmaxadd  12053  xrminmax  12057  xrbdtri  12068  climreu  12089  reccn2ap  12105  iserex  12131  climcvg1nlem  12141  serf0  12144  fz1f1o  12167  summodclem3  12173  zsumdc  12177  fsum3  12180  isumz  12182  isumss  12184  isumss2  12186  fsumsersdc  12188  fsum3ser  12190  fsumsplit  12200  isumclim2  12215  isumclim3  12216  fsum2dlemstep  12227  fsumcnv  12230  fisumcom2  12231  bcxmas  12282  isumle  12288  cvgratnnlemnexp  12317  cvgratnnlemmn  12318  cvgratz  12325  mertenslemub  12327  mertenslemi1  12328  mertenslem2  12329  mertensabs  12330  zproddc  12372  prod1dc  12379  fprodsplitdc  12389  fprodsplit  12390  fprodunsn  12397  fprodcl2lem  12398  fprodcllemf  12406  fprod2dlemstep  12415  fprodcnv  12418  fprodcom2fi  12419  fprodle  12433  ef0lem  12453  fsumdvds  12635  mod2eq1n2dvds  12672  ndvdssub  12723  bitsfzolem  12747  bitsfzo  12748  bitsinv1  12755  gcdsupex  12760  gcdsupcl  12761  bezoutlemnewy  12799  bezoutlemmain  12801  bezoutlembi  12808  bezoutlemeu  12810  bezoutlemle  12811  uzwodc  12840  nnwofdc  12841  nnwosdc  12842  nninfctlemfo  12843  nninfct  12844  nn0seqcvgd  12845  eucalgf  12859  eucalginv  12860  lcmval  12867  prmind2  12924  dfphi2  13028  phiprmpw  13030  phimullem  13033  eulerthlem1  13035  eulerthlemrprm  13037  eulerthlema  13038  eulerthlemh  13039  eulerthlemth  13040  eulerth  13041  phisum  13049  odzcllem  13051  odzdvds  13054  pythagtriplem19  13091  pclemub  13096  pcprecl  13098  pceu  13104  pcqmul  13112  pcqcl  13115  pcxnn0cl  13119  pcxqcl  13121  pcge0  13122  pcdvdsb  13129  pceq0  13131  pcneg  13134  pcdvdstr  13136  pcgcd1  13137  pc2dvds  13139  pcz  13141  pcprmpw2  13142  pcaddlem  13148  pcadd  13149  pcmptcl  13151  pcmpt  13152  pcmptdvds  13154  fldivp1  13157  qexpz  13161  pockthlem  13165  pockthg  13166  prmunb  13171  1arith  13176  4sqlemffi  13205  4sqlem17  13216  4sqlem18  13217  4sqlem19  13218  prmlem1a  13251  ballotfilemcdc  13282  ballotfilem2  13287  ballotfilemfp1  13290  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemfmpn  13293  ballotfilemefi  13296  ballotfilemiex  13303  ballotfilemro  13325  ennnfonelemom  13358  ennnfoneleminc  13361  ennnfonelemhf1o  13363  ennnfonelemex  13364  ennnfonelemhom  13365  ennnfonelemdm  13370  ennnfonelemr  13373  ennnfonelemim  13374  exmidunben  13376  ctinfom  13378  inffinp1  13379  ctinf  13380  enctlem  13382  ctiunctlemu1st  13384  ctiunctlemu2nd  13385  ctiunctlemudc  13387  ctiunct  13390  ctiunctal  13391  unct  13392  ssomct  13395  nninfdclemcl  13398  nninfdclemp1  13400  nninfdc  13403  structcnvcnv  13427  setscom  13451  relelbasov  13475  ressbas2d  13482  ressval3d  13486  ressabsg  13490  restid2  13662  imasaddfnlemg  13695  quslem  13705  ercpbl  13712  fnpr2ob  13721  mgmplusf  13746  grpinvalem  13765  grpinva  13766  grprida  13767  fngzsum  13768  gzsumvalx  13769  gzsum0  13773  gzsumval2  13774  ismnd  13792  mhmpropd  13833  grppropd  13882  grpsubf  13944  dfgrp3mlem  13963  mulgnn0p1  13996  mulgnn0subcl  13998  mulgsubcl  13999  mulgneg  14003  mulgnn0dir  14015  mulgnn0ass  14021  submmulg  14029  issubg2m  14052  issubg4m  14056  ghmmulg  14119  ghmrn  14120  gsumvalfi  14243  gzsumgsum  14246  gsumf1ofi  14251  gsummptfidmsplit  14255  gsumresfi  14264  gsummhmfi  14265  gsumressfi  14268  gsum2d2fi  14275  gsumcom2fi  14276  lringuplu  14613  rrgsupp  14684  opprdrng  14730  lmodscaf  14757  lssintclm  14831  lspun0  14872  lidlbas  14925  psrbagconcl  15178  gsumbagdiaglem  15180  psr1clfi  15203  topontopon  15258  eltg3i  15294  epttop  15328  difopn  15346  uncld  15351  0nnei  15391  resttopon  15409  restabs  15413  restopnb  15419  lmcvg  15455  cnptopco  15460  cnss1  15464  cnss2  15465  cncnpi  15466  cncnp2m  15469  cnrest  15473  cnrest2  15474  cnrest2r  15475  cnptoprest  15477  cnptoprest2  15478  lmss  15484  lmff  15487  lmtopcnp  15488  lmcn  15489  txbasval  15505  upxp  15510  txcnmpt  15511  txdis1cn  15516  txlm  15517  lmcn2  15518  cnmpt11  15521  cnmpt11f  15522  cnmpt1t  15523  cnmpt12  15525  cnmpt21  15529  cnmpt21f  15530  cnmpt2t  15531  cnmpt22  15532  cnmpt22f  15533  cnmptcom  15536  hmeocnv  15545  hmeof1o  15547  hmeores  15553  txhmeo  15557  txswaphmeo  15559  isxmet2d  15586  blfvalps  15623  xblss2ps  15642  xblss2  15643  blfps  15647  blf  15648  unirnblps  15660  unirnbl  15661  isxms2  15690  bdxmet  15739  bdmet  15740  xmetxp  15745  xmettx  15748  blssioo  15791  tgioo  15792  mulcncflem  15845  divcncfap  15852  dedekindeulemuub  15855  dedekindeulemub  15856  dedekindeulemloc  15857  dedekindeulemlu  15859  suplociccreex  15862  suplociccex  15863  dedekindicclemuub  15864  dedekindicclemub  15865  dedekindicclemloc  15866  dedekindicclemlu  15868  dedekindicc  15871  ivthinclemlopn  15874  ivthinclemuopn  15876  ivthdich  15891  limcrcl  15896  limcmpted  15901  limccnp2lem  15914  limccnp2cntop  15915  limccoap  15916  dvrecap  15951  plyaddlem1  15985  plymullem1  15986  plycoeid3  15995  plyco  15997  plycj  15999  plyrecj  16001  dvply1  16003  dvply2g  16004  cosordlem  16089  logbgcd1irraplemexp  16216  logbgcd1irrap  16218  zprmlogbaplem2  16228  zprmlogbaplem3  16229  birthdaylem2  16238  birthdaylem3  16239  chtqge0  16259  ppiprm  16271  ppinprm  16272  chtprm  16273  chtnprm  16274  chtqwordi  16275  ppiqltx  16293  bposlem2  16324  lgsneg1  16361  lgsdilem  16363  lgsdir2  16369  lgsdirprm  16370  lgsdir  16371  lgsne0  16374  lgsabs1  16375  lgsdirnn0  16383  lgsdinn0  16384  gausslemma2dlem1f1o  16396  gausslemma2dlem4  16400  lgseisenlem1  16406  lgsquadlem3  16415  2lgslem1a  16424  2sqlem5  16455  2sqlem7  16457  2sqlem8a  16458  2sqlem8  16459  2sqlem9  16460  gropeld  16507  grstructeld2dom  16508  uhgrm  16536  upgrm  16558  upgr1een  16582  uhgredgm  16594  edgupgren  16599  edgumgren  16600  edgusgren  16621  ausgrusgrben  16626  umgr2edg1  16667  usgredg2vlem1  16680  uhgr0enedgfi  16694  subupgr  16731  vtxedgfi  16747  vtxlpfi  16748  vtxdumgrfival  16756  vtxd0nedgbfi  16757  1hevtxdg0fi  16765  p1evtxdeqfilem  16769  wlkvtxm  16798  g0wlk0  16828  wlkres  16837  trlreslem  16847  clwwlkccatlem  16858  clwwlknnn  16870  trlsegvdeglem6  16923  eupth2lem3lem3fi  16928  eupth2lem3lem7fi  16932  eulerpathum  16939  dichmul0or  16977  bj-stand  16993  bj-charfundcALT  17052  bj-charfunbi  17054  bj-bdfindis  17190  bj-peano4  17198  strcollnfALT  17229  pw1map  17242  pwtrufal  17244  pwf1oexmid  17246  subctctexmid  17247  pw1nct  17250  stnot  17256  wexmiddc  17259  nnsf  17266  nninfalllem1  17269  nninfall  17270  nninfsellemqall  17276  nnnninfen  17282  exmidsbthrlem  17285  sbthom  17289  repiecef  17295  cvgcmp2nlemabs  17299  trilpo  17311  iswomni0  17320  redcwlpo  17324  dceqnconst  17329  dcapnconst  17330  nconstwlpolem  17334  nconstwlpo  17335  neapmkvlem  17336  neapmkv  17337  ltlenmkv  17339  taupi  17342  als1d  17352  als2d  17353  rals1d  17354  rals2d  17355  alseu1d  17388  alseu2d  17389  ralseu1d  17390  ralseu2d  17391  dfalseu2  17396