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  731  3mix3  1171  mpjao3dan  1320  ecase23d  1363  exlimdh  1620  nexd  1637  alexnim  1672  excomim  1687  19.41  1710  equcomd  1731  nfexd  1785  sbh  1800  sbcof2  1834  sbidm  1875  sb6rf  1877  nfsbt  2005  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  eu2  2099  2euex  2142  eqcomd  2212  3eltr3g  2291  abbid  2323  neneqd  2398  eqnetrrid  2408  3netr3g  2411  necomd  2463  r19.21bi  2595  nrexdv  2600  rexlimd  2621  rabbidva  2761  elisset  2787  euind  2961  rmoan  2974  reuind  2979  2rmorex  2980  spsbc  3011  spesbc  3085  eldifad  3178  eldifbd  3179  3sstr3g  3236  sseqtrdi  3242  difindiss  3428  un00  3508  undifss  3542  ifcldcd  3609  disjpr2  3698  difprsn1  3774  diftpsn3  3776  difsnss  3781  sneqr  3803  preqr1  3811  preq12b  3813  oprcl  3845  intab  3916  riinm  4002  rintm  4022  disjiun  4042  sndisj  4043  3brtr3g  4080  trint  4161  iinexgm  4202  exmidexmid  4244  exmid01  4246  pwntru  4247  exmid1stab  4256  pwel  4266  exss  4275  0nelop  4296  euotd  4303  opelopabsb  4310  pwunim  4337  issod  4370  frind  4403  suctr  4472  orduniss  4476  onelini  4481  oneluni  4482  eusv2i  4506  rexxfrd  4514  rabxfrd  4520  reuhypd  4522  iunpw  4531  sucexg  4550  ordsucim  4552  ordtriexmidlem  4571  ontriexmidim  4574  ordtri2or2exmidlem  4578  onsucelsucexmidlem  4581  ordsucunielexmid  4583  orddif  4599  suc11g  4609  onintexmid  4625  reg3exmidlemwe  4631  tfisi  4639  peano1  4646  peano2  4647  finds2  4653  omsinds  4674  brrelex12  4717  brel  4731  ssrel  4767  ssrel2  4769  ssrelrel  4779  elrel  4781  xpsspw  4791  relop  4832  dmxpm  4903  opelresi  4975  mptimass  5040  ndmima  5064  poirr2  5080  xpmlem  5108  xpimasn  5136  iotass  5254  iotacl  5261  dffun5r  5288  funeu  5301  funeu2  5302  funfnd  5307  funopg  5310  funun  5320  fununfun  5322  funinsn  5328  funtp  5332  funcnvuni  5348  funcnvres2  5354  imadiflem  5358  imadif  5359  funimaexglem  5362  fneu2  5386  fnimaeq0  5403  fnmpt  5408  fun2  5455  f00  5474  f0bi  5475  fimadmfo  5514  foimacnv  5547  resdif  5551  f1ococnv1  5558  fv3  5606  relelfvdm  5615  elfvm  5616  nfvres  5617  dffn5im  5631  mptfvex  5672  fvmptdf  5674  fvmptdv2  5676  fndmdif  5692  dff4im  5733  fmpt  5737  fmptd  5741  fmptdf  5744  f1oresrab  5752  fcoconst  5758  fsn  5759  funopsn  5769  ftpg  5775  fsnunf  5791  resfunexg  5812  isores1  5890  riota2df  5927  acexmidlemcase  5946  brabvv  5998  funoprabg  6051  fnovim  6061  ovmpodf  6084  ovi3  6090  elmpocl  6148  uchoice  6230  1stcof  6256  2ndcof  6257  fnmpo  6295  fmpoco  6309  fo2ndf  6320  f1o2ndf1  6321  disjxp1  6329  brtpos2  6344  reldmtpos  6346  dftpos3  6355  dftpos4  6356  tpostpos2  6358  tposf2  6361  tposf12  6362  tposfo  6364  tposf  6365  smores2  6387  tfrlem1  6401  tfrlem3-2d  6405  tfrlemisucaccv  6418  tfrlemibxssdm  6420  tfrlemibfn  6421  tfrlemi1  6425  tfrexlem  6427  tfr1onlemsucaccv  6434  tfr1onlembxssdm  6436  tfr1onlembfn  6437  tfr1onlemaccex  6441  tfrcllemsucaccv  6447  tfrcllembxssdm  6449  tfrcllembfn  6450  tfrcllemaccex  6454  tfrcldm  6456  rdgivallem  6474  rdgisucinc  6478  frecabex  6491  frecfnom  6494  frecfcllem  6497  frecsuclem  6499  omsuc  6565  nntri2  6587  nnsucuniel  6588  nnsseleq  6594  nnm00  6623  ecexr  6632  swoer  6655  elqsn0m  6697  iinerm  6701  erinxp  6703  ecinxp  6704  eroveu  6720  eroprf  6722  mapprc  6746  mapsn  6784  ixpprc  6813  ixp0  6825  resixp  6827  elixpsn  6829  dom2lem  6870  fundmen  6905  dom0  6942  xpf1o  6948  mapxpen  6952  xpmapenlem  6953  ssenen  6955  nneneq  6961  ssfilem  6979  dif1en  6983  dif1enen  6984  fin0  6989  fin0or  6990  diffitest  6991  diffisn  6997  ac6sfi  7002  fimax2gtrilemstep  7004  fimax2gtri  7005  finexdc  7006  exmidpweq  7013  pw1fin  7014  onunsnss  7021  unsnfidcel  7025  undifdcss  7027  undifdc  7028  tpfidceq  7034  fiintim  7035  fisseneq  7038  fidcenumlemr  7064  sbthlemi4  7069  sbthlemi5  7070  sbthlemi9  7074  fifo  7089  suplubti  7109  supelti  7111  infmoti  7137  infisoti  7141  djulclb  7164  updjud  7191  omp1eomlem  7203  0ct  7216  ctmlemr  7217  ctssdclemn0  7219  ctssdccl  7220  ctssdc  7222  enumct  7224  nninfninc  7232  nnnninfeq2  7238  finomni  7249  fodjuomnilemdc  7253  fodjum  7255  fodjuomnilemres  7257  fodjumkvlemres  7268  omniwomnimkv  7276  nninfwlporlem  7282  nninfwlpoimlemginf  7285  nninfwlpoim  7288  nninfinfwlpo  7289  ficardon  7303  exmidonfinlem  7308  en2eleq  7310  exmidfodomrlemeldju  7314  exmidfodomrlemreseldju  7315  exmidfodomrlemim  7316  finacn  7323  acfun  7326  exmidaclem  7327  exmidontriimlem3  7342  exmidontriimlem4  7343  exmidontriim  7344  pw1on  7345  dftap2  7370  2omotaplemst  7377  exmidapne  7379  ccfunen  7383  cc1  7384  cc2lem  7385  cc2  7386  cc3  7387  acnccim  7391  elni2  7434  indpi  7462  distrnqg  7507  subhalfnqq  7534  enq0sym  7552  enq0ref  7553  enq0tr  7554  nqnq0pi  7558  nnnq0lem1  7566  distrnq0  7579  elinp  7594  elnp1st2nd  7596  prltlu  7607  prnmaxl  7608  prnminu  7609  prarloc  7623  nqprm  7662  appdivnq  7683  prmuloc  7686  mullocpr  7691  distrlem4prl  7704  distrlem4pru  7705  ltexprlemm  7720  ltexprlemopl  7721  ltexprlemopu  7723  cauappcvgprlemopl  7766  cauappcvgprlemopu  7768  cauappcvgprlemdisj  7771  cauappcvgprlem2  7780  cauappcvgprlemlim  7781  caucvgprlemnkj  7786  caucvgprlemopl  7789  caucvgprlemopu  7791  caucvgprlemdisj  7794  caucvgprlemcl  7796  caucvgprlemladdfu  7797  caucvgprlemladdrl  7798  caucvgprlem2  7800  caucvgprprlemcbv  7807  caucvgprprlemval  7808  caucvgprprlemlol  7818  caucvgprprlemexbt  7826  caucvgprprlem1  7829  suplocexprlemrl  7837  suplocexprlemmu  7838  suplocexprlemru  7839  suplocexprlemdisj  7840  suplocexprlemloc  7841  suplocexprlemub  7843  suplocexprlemlub  7844  prsrlem1  7862  gt0srpr  7868  caucvgsrlemcl  7909  caucvgsrlembound  7914  caucvgsrlemgt1  7915  suplocsrlemb  7926  suplocsrlem  7928  suplocsr  7929  ltresr  7959  nnindnn  8013  axcaucvglemcl  8015  axcaucvglemval  8017  axcaucvglemcau  8018  axcaucvglemres  8019  axpre-suploclemres  8021  axpre-suploc  8022  sup3exmid  9037  nnind  9059  nn0supp  9354  nn0ge2m1nn  9362  zleloe  9426  zapne  9454  nn0lt2  9461  suprzclex  9478  zindd  9498  uzm1  9686  uzin  9688  infregelbex  9726  elnn1uz2  9735  nn01to3  9745  divfnzn  9749  qapne  9767  xrltnsym2  9923  xaddass  9998  xleadd1a  10002  xlt2add  10009  xlesubadd  10012  iooval2  10044  icoshftf1o  10120  fztri3or  10168  fzneuz  10230  4fvwrd4  10269  elfzo0  10313  infssuzex  10383  infssuzcldc  10385  suprzubdc  10386  nninfdcex  10387  zsupssdc  10388  exbtwnzlemex  10399  ioom  10410  fzfig  10582  uzennn  10588  uzsinds  10596  iseqovex  10610  seq3val  10612  seqvalcd  10613  seqf  10616  seqovcd  10619  monoord2  10638  iseqf1olemjpcl  10660  iseqf1olemqpcl  10661  seq3f1olemqsum  10665  seq3f1o  10669  seqf1og  10673  seq3distr  10684  expp1  10698  expcl2lemap  10703  expclzap  10716  expap0i  10723  nn0ltexp2  10861  bcval5  10915  hashinfuni  10929  hashennnuni  10931  hashnncl  10947  resunimafz0  10983  zfz1isolemiso  10991  zfz1isolem1  10992  zfz1iso  10993  wrdsymb0  11033  wrdlen1  11038  ccat1st1st  11101  swrdrlen  11122  pfxid  11145  pfxwrdsymbg  11149  pfxtrcfv  11152  pfxccat1  11161  pfxpfxid  11168  seq3shft  11193  cvg1nlemcau  11339  rexanuz  11343  resqrexlemoverl  11376  resqrexlemglsq  11377  resqrexlemsqa  11379  resqrexlemex  11380  rersqreu  11383  caubnd2  11472  maxleast  11568  fimaxre2  11582  minmax  11585  xrmaxiflemcl  11600  xrmaxiflemab  11602  xrmaxiflemlub  11603  xrmaxadd  11616  xrminmax  11620  xrbdtri  11631  climreu  11652  reccn2ap  11668  iserex  11694  climcvg1nlem  11704  serf0  11707  fz1f1o  11730  summodclem3  11735  zsumdc  11739  fsum3  11742  isumz  11744  isumss  11746  isumss2  11748  fsumsersdc  11750  fsum3ser  11752  fsumsplit  11762  isumclim2  11777  isumclim3  11778  fsum2dlemstep  11789  fsumcnv  11792  fisumcom2  11793  bcxmas  11844  isumle  11850  cvgratnnlemnexp  11879  cvgratnnlemmn  11880  cvgratz  11887  mertenslemub  11889  mertenslemi1  11890  mertenslem2  11891  mertensabs  11892  zproddc  11934  prod1dc  11941  fprodsplitdc  11951  fprodsplit  11952  fprodunsn  11959  fprodcl2lem  11960  fprodcllemf  11968  fprod2dlemstep  11977  fprodcnv  11980  fprodcom2fi  11981  fprodle  11995  ef0lem  12015  fsumdvds  12197  mod2eq1n2dvds  12234  ndvdssub  12285  bitsfzolem  12309  bitsfzo  12310  bitsinv1  12317  gcdsupex  12322  gcdsupcl  12323  bezoutlemnewy  12361  bezoutlemmain  12363  bezoutlembi  12370  bezoutlemeu  12372  bezoutlemle  12373  uzwodc  12402  nnwofdc  12403  nnwosdc  12404  nninfctlemfo  12405  nninfct  12406  nn0seqcvgd  12407  eucalgf  12421  eucalginv  12422  lcmval  12429  prmind2  12486  dfphi2  12586  phiprmpw  12588  phimullem  12591  eulerthlem1  12593  eulerthlemrprm  12595  eulerthlema  12596  eulerthlemh  12597  eulerthlemth  12598  eulerth  12599  phisum  12607  odzcllem  12609  odzdvds  12612  pythagtriplem19  12649  pclemub  12654  pcprecl  12656  pceu  12662  pcqmul  12670  pcqcl  12673  pcxnn0cl  12677  pcxqcl  12679  pcge0  12680  pcdvdsb  12687  pceq0  12689  pcneg  12692  pcdvdstr  12694  pcgcd1  12695  pc2dvds  12697  pcz  12699  pcprmpw2  12700  pcaddlem  12706  pcadd  12707  pcmptcl  12709  pcmpt  12710  pcmptdvds  12712  fldivp1  12715  qexpz  12719  pockthlem  12723  pockthg  12724  prmunb  12729  1arith  12734  4sqlemffi  12763  4sqlem17  12774  4sqlem18  12775  4sqlem19  12776  ennnfonelemom  12823  ennnfoneleminc  12826  ennnfonelemhf1o  12828  ennnfonelemex  12829  ennnfonelemhom  12830  ennnfonelemdm  12835  ennnfonelemr  12838  ennnfonelemim  12839  exmidunben  12841  ctinfom  12843  inffinp1  12844  ctinf  12845  enctlem  12847  ctiunctlemu1st  12849  ctiunctlemu2nd  12850  ctiunctlemudc  12852  ctiunct  12855  ctiunctal  12856  unct  12857  ssomct  12860  nninfdclemcl  12863  nninfdclemp1  12865  nninfdc  12868  structcnvcnv  12892  setscom  12916  relelbasov  12938  ressbas2d  12944  ressval3d  12948  ressabsg  12952  restid2  13124  imasaddfnlemg  13190  quslem  13200  ercpbl  13207  fnpr2ob  13216  mgmplusf  13242  grpinvalem  13261  grpinva  13262  grprida  13263  fngsum  13264  igsumvalx  13265  gsum0g  13272  gsumval2  13273  ismnd  13295  mhmpropd  13342  grppropd  13393  grpsubf  13455  dfgrp3mlem  13474  mulgnn0p1  13513  mulgnn0subcl  13515  mulgsubcl  13516  mulgneg  13520  mulgnn0dir  13532  mulgnn0ass  13538  submmulg  13546  issubg2m  13569  issubg4m  13573  ghmmulg  13636  ghmrn  13637  lringuplu  14002  lmodscaf  14116  lssintclm  14190  lspun0  14231  lidlbas  14284  psr1clfi  14494  topontopon  14536  eltg3i  14572  epttop  14606  difopn  14624  uncld  14629  0nnei  14669  resttopon  14687  restabs  14691  restopnb  14697  lmcvg  14733  cnptopco  14738  cnss1  14742  cnss2  14743  cncnpi  14744  cncnp2m  14747  cnrest  14751  cnrest2  14752  cnrest2r  14753  cnptoprest  14755  cnptoprest2  14756  lmss  14762  lmff  14765  lmtopcnp  14766  lmcn  14767  txbasval  14783  upxp  14788  txcnmpt  14789  txdis1cn  14794  txlm  14795  lmcn2  14796  cnmpt11  14799  cnmpt11f  14800  cnmpt1t  14801  cnmpt12  14803  cnmpt21  14807  cnmpt21f  14808  cnmpt2t  14809  cnmpt22  14810  cnmpt22f  14811  cnmptcom  14814  hmeocnv  14823  hmeof1o  14825  hmeores  14831  txhmeo  14835  txswaphmeo  14837  isxmet2d  14864  blfvalps  14901  xblss2ps  14920  xblss2  14921  blfps  14925  blf  14926  unirnblps  14938  unirnbl  14939  isxms2  14968  bdxmet  15017  bdmet  15018  xmetxp  15023  xmettx  15026  blssioo  15069  tgioo  15070  mulcncflem  15123  divcncfap  15130  dedekindeulemuub  15133  dedekindeulemub  15134  dedekindeulemloc  15135  dedekindeulemlu  15137  suplociccreex  15140  suplociccex  15141  dedekindicclemuub  15142  dedekindicclemub  15143  dedekindicclemloc  15144  dedekindicclemlu  15146  dedekindicc  15149  ivthinclemlopn  15152  ivthinclemuopn  15154  ivthdich  15169  limcrcl  15174  limcmpted  15179  limccnp2lem  15192  limccnp2cntop  15193  limccoap  15194  dvrecap  15229  plyaddlem1  15263  plymullem1  15264  plycoeid3  15273  plyco  15275  plycj  15277  plyrecj  15279  dvply1  15281  dvply2g  15282  cosordlem  15365  logbgcd1irraplemexp  15484  logbgcd1irrap  15486  lgsneg1  15546  lgsdilem  15548  lgsdir2  15554  lgsdirprm  15555  lgsdir  15556  lgsne0  15559  lgsabs1  15560  lgsdirnn0  15568  lgsdinn0  15569  gausslemma2dlem1f1o  15581  gausslemma2dlem4  15585  lgseisenlem1  15591  lgsquadlem3  15600  2lgslem1a  15609  2sqlem5  15640  2sqlem7  15642  2sqlem8a  15643  2sqlem8  15644  2sqlem9  15645  gropeld  15692  grstructeld2dom  15693  uhgrm  15718  bj-stand  15758  bj-charfundcALT  15819  bj-charfunbi  15821  bj-bdfindis  15957  bj-peano4  15965  strcollnfALT  15996  1dom1el  16001  2omap  16006  pwtrufal  16008  pwf1oexmid  16010  subctctexmid  16011  pw1nct  16014  nnsf  16016  nninfalllem1  16019  nninfall  16020  nninfsellemqall  16026  nnnninfen  16032  exmidsbthrlem  16035  sbthom  16039  cvgcmp2nlemabs  16045  trilpo  16056  iswomni0  16064  redcwlpo  16068  dceqnconst  16073  dcapnconst  16074  nconstwlpolem  16078  nconstwlpo  16079  neapmkvlem  16080  neapmkv  16081  ltlenmkv  16083  taupi  16086  alsi1d  16094  alsi2d  16095  alsc1d  16096  alsc2d  16097