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  733  3mix3  1173  mpjao3dan  1322  ecase23d  1365  exlimdh  1622  nexd  1639  alexnim  1674  excomim  1689  19.41  1712  equcomd  1733  nfexd  1787  sbh  1802  sbcof2  1836  sbidm  1877  sb6rf  1879  nfsbt  2007  dvelimALT  2041  dvelimfv  2042  dvelimor  2049  eu2  2102  2euex  2145  eqcomd  2215  3eltr3g  2294  abbid  2326  neneqd  2401  eqnetrrid  2411  3netr3g  2414  necomd  2466  r19.21bi  2598  nrexdv  2603  rexlimd  2625  rabbidva  2767  elisset  2794  euind  2970  rmoan  2983  reuind  2988  2rmorex  2989  spsbc  3020  spesbc  3095  eldifad  3188  eldifbd  3189  3sstr3g  3246  sseqtrdi  3252  difindiss  3438  un00  3518  undifss  3552  ifcldcd  3620  disjpr2  3710  difprsn1  3786  diftpsn3  3788  difsnss  3793  sneqr  3817  preqr1  3825  preq12b  3827  oprcl  3860  intab  3931  riinm  4017  rintm  4037  disjiun  4057  sndisj  4058  3brtr3g  4095  trint  4176  iinexgm  4217  exmidexmid  4259  exmid01  4261  pwntru  4262  exmid1stab  4271  pwel  4283  exss  4292  0nelop  4313  euotd  4320  opelopabsb  4327  pwunim  4354  issod  4387  frind  4420  suctr  4489  orduniss  4493  onelini  4498  oneluni  4499  eusv2i  4523  rexxfrd  4531  rabxfrd  4537  reuhypd  4539  iunpw  4548  sucexg  4567  ordsucim  4569  ordtriexmidlem  4588  ontriexmidim  4591  ordtri2or2exmidlem  4595  onsucelsucexmidlem  4598  ordsucunielexmid  4600  orddif  4616  suc11g  4626  onintexmid  4642  reg3exmidlemwe  4648  tfisi  4656  peano1  4663  peano2  4664  finds2  4670  omsinds  4691  brrelex12  4734  brel  4748  ssrel  4784  ssrel2  4786  ssrelrel  4796  elrel  4798  xpsspw  4808  relop  4849  dmxpm  4920  opelresi  4992  mptimass  5057  ndmima  5081  poirr2  5097  xpmlem  5125  xpimasn  5153  iotass  5272  iotacl  5279  dffun5r  5306  funeu  5319  funeu2  5320  funfnd  5325  funopg  5328  funun  5338  fununfun  5340  funinsn  5346  funtp  5350  funcnvuni  5366  funcnvres2  5372  imadiflem  5376  imadif  5377  funimaexglem  5380  fneu2  5404  fnimaeq0  5421  fnmpt  5426  fun2  5474  f00  5493  f0bi  5494  fimadmfo  5533  foimacnv  5566  resdif  5570  f1ococnv1  5577  fv3  5626  relelfvdm  5635  elfvm  5636  nfvres  5637  dffn5im  5652  mptfvex  5693  fvmptdf  5695  fvmptdv2  5697  fndmdif  5713  dff4im  5754  fmpt  5758  fmptd  5762  fmptdf  5765  f1oresrab  5773  fcoconst  5779  fsn  5780  funopsn  5790  ftpg  5796  fsnunf  5812  resfunexg  5833  isores1  5911  riota2df  5949  acexmidlemcase  5969  brabvv  6021  funoprabg  6074  fnovim  6084  ovmpodf  6107  ovi3  6113  elmpocl  6171  uchoice  6253  1stcof  6279  2ndcof  6280  fnmpo  6318  fmpoco  6332  fo2ndf  6343  f1o2ndf1  6344  disjxp1  6352  brtpos2  6367  reldmtpos  6369  dftpos3  6378  dftpos4  6379  tpostpos2  6381  tposf2  6384  tposf12  6385  tposfo  6387  tposf  6388  smores2  6410  tfrlem1  6424  tfrlem3-2d  6428  tfrlemisucaccv  6441  tfrlemibxssdm  6443  tfrlemibfn  6444  tfrlemi1  6448  tfrexlem  6450  tfr1onlemsucaccv  6457  tfr1onlembxssdm  6459  tfr1onlembfn  6460  tfr1onlemaccex  6464  tfrcllemsucaccv  6470  tfrcllembxssdm  6472  tfrcllembfn  6473  tfrcllemaccex  6477  tfrcldm  6479  rdgivallem  6497  rdgisucinc  6501  frecabex  6514  frecfnom  6517  frecfcllem  6520  frecsuclem  6522  omsuc  6588  nntri2  6610  nnsucuniel  6611  nnsseleq  6617  nnm00  6646  ecexr  6655  swoer  6678  elqsn0m  6720  iinerm  6724  erinxp  6726  ecinxp  6727  eroveu  6743  eroprf  6745  mapprc  6769  mapsn  6807  ixpprc  6836  ixp0  6848  resixp  6850  elixpsn  6852  dom2lem  6893  fundmen  6929  dom0  6967  xpf1o  6973  mapxpen  6977  xpmapenlem  6978  ssenen  6980  nneneq  6986  ssfilem  7005  dif1en  7009  dif1enen  7010  fin0  7015  fin0or  7016  diffitest  7017  diffisn  7023  ac6sfi  7028  fimax2gtrilemstep  7030  fimax2gtri  7031  finexdc  7032  exmidpweq  7039  pw1fin  7040  onunsnss  7047  unsnfidcel  7051  undifdcss  7053  undifdc  7054  tpfidceq  7060  fiintim  7061  fisseneq  7064  fidcenumlemr  7090  sbthlemi4  7095  sbthlemi5  7096  sbthlemi9  7100  fifo  7115  suplubti  7135  supelti  7137  infmoti  7163  infisoti  7167  djulclb  7190  updjud  7217  omp1eomlem  7229  0ct  7242  ctmlemr  7243  ctssdclemn0  7245  ctssdccl  7246  ctssdc  7248  enumct  7250  nninfninc  7258  nnnninfeq2  7264  finomni  7275  fodjuomnilemdc  7279  fodjum  7281  fodjuomnilemres  7283  fodjumkvlemres  7294  omniwomnimkv  7302  nninfwlporlem  7308  nninfwlpoimlemginf  7311  nninfwlpoim  7314  nninfinfwlpo  7315  ficardon  7329  pr2cv1  7336  exmidonfinlem  7339  en2eleq  7341  exmidfodomrlemeldju  7345  exmidfodomrlemreseldju  7346  exmidfodomrlemim  7347  finacn  7354  acfun  7357  exmidaclem  7358  exmidontriimlem3  7373  exmidontriimlem4  7374  exmidontriim  7375  pw1if  7378  pw1on  7379  dftap2  7405  2omotaplemst  7412  exmidapne  7414  ccfunen  7418  cc1  7419  cc2lem  7420  cc2  7421  cc3  7422  acnccim  7426  elni2  7469  indpi  7497  distrnqg  7542  subhalfnqq  7569  enq0sym  7587  enq0ref  7588  enq0tr  7589  nqnq0pi  7593  nnnq0lem1  7601  distrnq0  7614  elinp  7629  elnp1st2nd  7631  prltlu  7642  prnmaxl  7643  prnminu  7644  prarloc  7658  nqprm  7697  appdivnq  7718  prmuloc  7721  mullocpr  7726  distrlem4prl  7739  distrlem4pru  7740  ltexprlemm  7755  ltexprlemopl  7756  ltexprlemopu  7758  cauappcvgprlemopl  7801  cauappcvgprlemopu  7803  cauappcvgprlemdisj  7806  cauappcvgprlem2  7815  cauappcvgprlemlim  7816  caucvgprlemnkj  7821  caucvgprlemopl  7824  caucvgprlemopu  7826  caucvgprlemdisj  7829  caucvgprlemcl  7831  caucvgprlemladdfu  7832  caucvgprlemladdrl  7833  caucvgprlem2  7835  caucvgprprlemcbv  7842  caucvgprprlemval  7843  caucvgprprlemlol  7853  caucvgprprlemexbt  7861  caucvgprprlem1  7864  suplocexprlemrl  7872  suplocexprlemmu  7873  suplocexprlemru  7874  suplocexprlemdisj  7875  suplocexprlemloc  7876  suplocexprlemub  7878  suplocexprlemlub  7879  prsrlem1  7897  gt0srpr  7903  caucvgsrlemcl  7944  caucvgsrlembound  7949  caucvgsrlemgt1  7950  suplocsrlemb  7961  suplocsrlem  7963  suplocsr  7964  ltresr  7994  nnindnn  8048  axcaucvglemcl  8050  axcaucvglemval  8052  axcaucvglemcau  8053  axcaucvglemres  8054  axpre-suploclemres  8056  axpre-suploc  8057  sup3exmid  9072  nnind  9094  nn0supp  9389  nn0ge2m1nn  9397  zleloe  9461  zapne  9489  nn0lt2  9496  suprzclex  9513  zindd  9533  uzm1  9721  uzin  9723  infregelbex  9761  elnn1uz2  9770  nn01to3  9780  divfnzn  9784  qapne  9802  xrltnsym2  9958  xaddass  10033  xleadd1a  10037  xlt2add  10044  xlesubadd  10047  iooval2  10079  icoshftf1o  10155  fztri3or  10203  fzneuz  10265  4fvwrd4  10304  elfzo0  10350  infssuzex  10420  infssuzcldc  10422  suprzubdc  10423  nninfdcex  10424  zsupssdc  10425  exbtwnzlemex  10436  ioom  10447  fzfig  10619  uzennn  10625  uzsinds  10633  iseqovex  10647  seq3val  10649  seqvalcd  10650  seqf  10653  seqovcd  10656  monoord2  10675  iseqf1olemjpcl  10697  iseqf1olemqpcl  10698  seq3f1olemqsum  10702  seq3f1o  10706  seqf1og  10710  seq3distr  10721  expp1  10735  expcl2lemap  10740  expclzap  10753  expap0i  10760  nn0ltexp2  10898  bcval5  10952  hashinfuni  10966  hashennnuni  10968  hashnncl  10984  resunimafz0  11020  zfz1isolemiso  11028  zfz1isolem1  11029  zfz1iso  11030  wrdsymb0  11070  wrdlen1  11075  ccat1st1st  11138  swrdrlen  11159  pfxid  11184  pfxwrdsymbg  11188  pfxtrcfv  11191  pfxccat1  11200  pfxpfxid  11207  pfxcctswrd  11208  swrdccatin1  11223  pfxccatin12  11231  pfxccatid  11239  seq3shft  11315  cvg1nlemcau  11461  rexanuz  11465  resqrexlemoverl  11498  resqrexlemglsq  11499  resqrexlemsqa  11501  resqrexlemex  11502  rersqreu  11505  caubnd2  11594  maxleast  11690  fimaxre2  11704  minmax  11707  xrmaxiflemcl  11722  xrmaxiflemab  11724  xrmaxiflemlub  11725  xrmaxadd  11738  xrminmax  11742  xrbdtri  11753  climreu  11774  reccn2ap  11790  iserex  11816  climcvg1nlem  11826  serf0  11829  fz1f1o  11852  summodclem3  11857  zsumdc  11861  fsum3  11864  isumz  11866  isumss  11868  isumss2  11870  fsumsersdc  11872  fsum3ser  11874  fsumsplit  11884  isumclim2  11899  isumclim3  11900  fsum2dlemstep  11911  fsumcnv  11914  fisumcom2  11915  bcxmas  11966  isumle  11972  cvgratnnlemnexp  12001  cvgratnnlemmn  12002  cvgratz  12009  mertenslemub  12011  mertenslemi1  12012  mertenslem2  12013  mertensabs  12014  zproddc  12056  prod1dc  12063  fprodsplitdc  12073  fprodsplit  12074  fprodunsn  12081  fprodcl2lem  12082  fprodcllemf  12090  fprod2dlemstep  12099  fprodcnv  12102  fprodcom2fi  12103  fprodle  12117  ef0lem  12137  fsumdvds  12319  mod2eq1n2dvds  12356  ndvdssub  12407  bitsfzolem  12431  bitsfzo  12432  bitsinv1  12439  gcdsupex  12444  gcdsupcl  12445  bezoutlemnewy  12483  bezoutlemmain  12485  bezoutlembi  12492  bezoutlemeu  12494  bezoutlemle  12495  uzwodc  12524  nnwofdc  12525  nnwosdc  12526  nninfctlemfo  12527  nninfct  12528  nn0seqcvgd  12529  eucalgf  12543  eucalginv  12544  lcmval  12551  prmind2  12608  dfphi2  12708  phiprmpw  12710  phimullem  12713  eulerthlem1  12715  eulerthlemrprm  12717  eulerthlema  12718  eulerthlemh  12719  eulerthlemth  12720  eulerth  12721  phisum  12729  odzcllem  12731  odzdvds  12734  pythagtriplem19  12771  pclemub  12776  pcprecl  12778  pceu  12784  pcqmul  12792  pcqcl  12795  pcxnn0cl  12799  pcxqcl  12801  pcge0  12802  pcdvdsb  12809  pceq0  12811  pcneg  12814  pcdvdstr  12816  pcgcd1  12817  pc2dvds  12819  pcz  12821  pcprmpw2  12822  pcaddlem  12828  pcadd  12829  pcmptcl  12831  pcmpt  12832  pcmptdvds  12834  fldivp1  12837  qexpz  12841  pockthlem  12845  pockthg  12846  prmunb  12851  1arith  12856  4sqlemffi  12885  4sqlem17  12896  4sqlem18  12897  4sqlem19  12898  ennnfonelemom  12945  ennnfoneleminc  12948  ennnfonelemhf1o  12950  ennnfonelemex  12951  ennnfonelemhom  12952  ennnfonelemdm  12957  ennnfonelemr  12960  ennnfonelemim  12961  exmidunben  12963  ctinfom  12965  inffinp1  12966  ctinf  12967  enctlem  12969  ctiunctlemu1st  12971  ctiunctlemu2nd  12972  ctiunctlemudc  12974  ctiunct  12977  ctiunctal  12978  unct  12979  ssomct  12982  nninfdclemcl  12985  nninfdclemp1  12987  nninfdc  12990  structcnvcnv  13014  setscom  13038  relelbasov  13061  ressbas2d  13067  ressval3d  13071  ressabsg  13075  restid2  13247  imasaddfnlemg  13313  quslem  13323  ercpbl  13330  fnpr2ob  13339  mgmplusf  13365  grpinvalem  13384  grpinva  13385  grprida  13386  fngsum  13387  igsumvalx  13388  gsum0g  13395  gsumval2  13396  ismnd  13418  mhmpropd  13465  grppropd  13516  grpsubf  13578  dfgrp3mlem  13597  mulgnn0p1  13636  mulgnn0subcl  13638  mulgsubcl  13639  mulgneg  13643  mulgnn0dir  13655  mulgnn0ass  13661  submmulg  13669  issubg2m  13692  issubg4m  13696  ghmmulg  13759  ghmrn  13760  lringuplu  14125  lmodscaf  14239  lssintclm  14313  lspun0  14354  lidlbas  14407  psr1clfi  14617  topontopon  14659  eltg3i  14695  epttop  14729  difopn  14747  uncld  14752  0nnei  14792  resttopon  14810  restabs  14814  restopnb  14820  lmcvg  14856  cnptopco  14861  cnss1  14865  cnss2  14866  cncnpi  14867  cncnp2m  14870  cnrest  14874  cnrest2  14875  cnrest2r  14876  cnptoprest  14878  cnptoprest2  14879  lmss  14885  lmff  14888  lmtopcnp  14889  lmcn  14890  txbasval  14906  upxp  14911  txcnmpt  14912  txdis1cn  14917  txlm  14918  lmcn2  14919  cnmpt11  14922  cnmpt11f  14923  cnmpt1t  14924  cnmpt12  14926  cnmpt21  14930  cnmpt21f  14931  cnmpt2t  14932  cnmpt22  14933  cnmpt22f  14934  cnmptcom  14937  hmeocnv  14946  hmeof1o  14948  hmeores  14954  txhmeo  14958  txswaphmeo  14960  isxmet2d  14987  blfvalps  15024  xblss2ps  15043  xblss2  15044  blfps  15048  blf  15049  unirnblps  15061  unirnbl  15062  isxms2  15091  bdxmet  15140  bdmet  15141  xmetxp  15146  xmettx  15149  blssioo  15192  tgioo  15193  mulcncflem  15246  divcncfap  15253  dedekindeulemuub  15256  dedekindeulemub  15257  dedekindeulemloc  15258  dedekindeulemlu  15260  suplociccreex  15263  suplociccex  15264  dedekindicclemuub  15265  dedekindicclemub  15266  dedekindicclemloc  15267  dedekindicclemlu  15269  dedekindicc  15272  ivthinclemlopn  15275  ivthinclemuopn  15277  ivthdich  15292  limcrcl  15297  limcmpted  15302  limccnp2lem  15315  limccnp2cntop  15316  limccoap  15317  dvrecap  15352  plyaddlem1  15386  plymullem1  15387  plycoeid3  15396  plyco  15398  plycj  15400  plyrecj  15402  dvply1  15404  dvply2g  15405  cosordlem  15488  logbgcd1irraplemexp  15607  logbgcd1irrap  15609  lgsneg1  15669  lgsdilem  15671  lgsdir2  15677  lgsdirprm  15678  lgsdir  15679  lgsne0  15682  lgsabs1  15683  lgsdirnn0  15691  lgsdinn0  15692  gausslemma2dlem1f1o  15704  gausslemma2dlem4  15708  lgseisenlem1  15714  lgsquadlem3  15723  2lgslem1a  15732  2sqlem5  15763  2sqlem7  15765  2sqlem8a  15766  2sqlem8  15767  2sqlem9  15768  gropeld  15815  grstructeld2dom  15816  uhgrm  15843  upgrm  15865  uhgredgm  15899  edgupgren  15904  edgumgren  15905  edgusgren  15926  ausgrusgrben  15931  umgr2edg1  15972  usgredg2vlem1  15985  bj-stand  16022  bj-charfundcALT  16082  bj-charfunbi  16084  bj-bdfindis  16220  bj-peano4  16228  strcollnfALT  16259  1dom1el  16264  2omap  16270  pw1map  16272  pwtrufal  16274  pwf1oexmid  16276  subctctexmid  16277  pw1nct  16280  nnsf  16282  nninfalllem1  16285  nninfall  16286  nninfsellemqall  16292  nnnninfen  16298  exmidsbthrlem  16301  sbthom  16305  cvgcmp2nlemabs  16311  trilpo  16322  iswomni0  16330  redcwlpo  16334  dceqnconst  16339  dcapnconst  16340  nconstwlpolem  16344  nconstwlpo  16345  neapmkvlem  16346  neapmkv  16347  ltlenmkv  16349  taupi  16352  alsi1d  16360  alsi2d  16361  alsc1d  16362  alsc2d  16363