Theorem sylib 127

Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by NM, 5-Aug-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 113	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  bicomd  129  pm5.74d  171  bitri  173  3imtr3i  189  ancomd  254  pm4.71d  373  pm4.71rd  374  imdistand  421  orcomd  648  3mix3  1075  mpjao3dan  1202  ecase23d  1240  exlimdh  1487  nexd  1504  alexnim  1539  excomim  1553  19.41  1576  nfexd  1644  sbh  1659  sbcof2  1691  sbidm  1731  sb6rf  1733  nfsbt  1850  dvelimALT  1886  dvelimfv  1887  dvelimor  1894  eu2  1944  2euex  1987  eqcomd  2045  3eltr3g  2122  abbid  2154  neneqd  2226  syl5eqner  2236  3netr3g  2239  necomd  2291  r19.21bi  2407  nrexdv  2412  rexlimd  2430  rabbidva  2548  elisset  2568  euind  2728  rmoan  2739  reuind  2744  2rmorex  2745  spsbc  2775  spesbc  2843  eldifad  2929  eldifbd  2930  3sstr3g  2985  syl6sseq  2991  difindiss  3191  un00  3263  disjpss  3278  undifss  3303  ifcldcd  3358  disjpr2  3434  difprsn1  3503  diftpsn3  3505  difsnpssim  3507  difsnss  3510  sneqr  3531  preqr1  3539  preq12b  3541  oprcl  3573  intab  3644  riinm  3729  rintm  3744  sndisj  3760  3brtr3g  3795  trint  3869  iinexgm  3908  pwel  3954  exss  3963  0nelop  3985  euotd  3991  opelopabsb  3997  pwunim  4023  issod  4056  frind  4089  suctr  4158  orduniss  4162  onelini  4167  oneluni  4168  eusv2i  4187  rexxfrd  4195  rabxfrd  4201  reuhypd  4203  iunpw  4211  sucexg  4224  ordsucim  4226  ordtriexmidlem  4245  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  ordsucunielexmid  4256  orddif  4271  suc11g  4281  onintexmid  4297  reg3exmidlemwe  4303  tfisi  4310  peano1  4317  peano2  4318  finds2  4324  brrelex12  4381  brel  4392  ssrel  4428  ssrel2  4430  ssrelrel  4440  elrel  4442  xpsspw  4450  relop  4486  dmxpm  4555  opelresi  4623  ndmima  4702  poirr2  4717  xpmlem  4744  xpimasn  4769  iotass  4884  iotacl  4890  dffun5r  4914  funeu  4926  funeu2  4927  funopg  4934  funun  4944  funtp  4952  funcnvuni  4968  funcnvres2  4974  imadiflem  4978  imadif  4979  funimaexglem  4982  fneu2  5004  fnimaeq0  5020  fnmpt  5025  fun2  5064  f00  5081  foimacnv  5144  resdif  5148  f1ococnv1  5155  fv3  5197  relelfvdm  5205  nfvres  5206  dffn5im  5219  mptfvex  5256  fvmptdf  5258  fvmptdv2  5260  fndmdif  5272  dff4im  5313  fmpt  5319  fmptd  5322  f1oresrab  5329  fcoconst  5334  fsn  5335  ftpg  5347  fsnunf  5362  resfunexg  5382  isores1  5454  riota2df  5488  acexmidlemcase  5507  brabvv  5551  funoprabg  5600  fnovim  5609  ovmpt2df  5632  ovi3  5637  grprinvlem  5695  grprinvd  5696  grpridd  5697  elmpt2cl  5698  1stcof  5790  2ndcof  5791  fnmpt2  5828  fmpt2co  5837  fo2ndf  5848  f1o2ndf1  5849  brtpos2  5866  reldmtpos  5868  dftpos3  5877  dftpos4  5878  tpostpos2  5880  tposf2  5883  tposf12  5884  tposfo  5886  tposf  5887  smores2  5909  tfrlem1  5923  tfrlem3-2d  5928  tfrlemisucaccv  5939  tfrlemibxssdm  5941  tfrlemibfn  5942  tfrlemi1  5946  tfrexlem  5948  rdgivallem  5968  rdgisucinc  5972  rdgon  5973  frecabex  5984  frecfnom  5986  frecsuclemdm  5988  freccl  5993  omsuc  6051  nntri2  6073  nnsseleq  6079  nndifsnid  6080  nnm00  6102  ecexr  6111  swoer  6134  elqsn0m  6174  iinerm  6178  erinxp  6180  ecinxp  6181  eroveu  6197  eroprf  6199  dom2lem  6252  fundmen  6286  nneneq  6320  fidifsnid  6332  ssfiexmid  6336  dif1en  6337  fin0  6342  fin0or  6343  diffitest  6344  diffisn  6350  ac6sfi  6352  onunsnss  6355  elni2  6412  indpi  6440  distrnqg  6485  subhalfnqq  6512  enq0sym  6530  enq0ref  6531  enq0tr  6532  nqnq0pi  6536  nnnq0lem1  6544  distrnq0  6557  elinp  6572  elnp1st2nd  6574  prltlu  6585  prnmaxl  6586  prnminu  6587  prarloc  6601  nqprm  6640  appdivnq  6661  prmuloc  6664  mullocpr  6669  distrlem4prl  6682  distrlem4pru  6683  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemopu  6701  cauappcvgprlemopl  6744  cauappcvgprlemopu  6746  cauappcvgprlemdisj  6749  cauappcvgprlem2  6758  cauappcvgprlemlim  6759  caucvgprlemnkj  6764  caucvgprlemopl  6767  caucvgprlemopu  6769  caucvgprlemdisj  6772  caucvgprlemcl  6774  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlem2  6778  caucvgprprlemcbv  6785  caucvgprprlemval  6786  caucvgprprlemlol  6796  caucvgprprlemexbt  6804  caucvgprprlem1  6807  prsrlem1  6827  gt0srpr  6833  caucvgsrlemcl  6873  caucvgsrlembound  6878  caucvgsrlemgt1  6879  ltresr  6915  nnindnn  6967  axcaucvglemcl  6969  axcaucvglemval  6971  axcaucvglemcau  6972  axcaucvglemres  6973  nnind  7930  nn0supp  8234  nn0ge2m1nn  8242  zleloe  8292  zapne  8315  nn0lt2  8322  zindd  8356  uzm1  8503  uzin  8505  elnn1uz2  8544  nn01to3  8552  divfnzn  8556  qapne  8574  xrltnsym2  8715  iooval2  8784  icoshftf1o  8859  fztri3or  8903  fzneuz  8963  4fvwrd4  8997  elfzo0  9038  fzfig  9206  iseqovex  9219  iseqval  9220  monoord2  9236  iseqdistr  9249  expivallem  9256  expival  9257  expp1  9262  expcl2lemap  9267  expclzap  9280  expap0i  9287  cvg1nlemcau  9583  rexanuz  9587  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemsqa  9622  resqrexlemex  9623  rersqreu  9626  caubnd2  9713  climreu  9818  iiserex  9859  climcvg1nlem  9868  serif0  9871  nn0seqcvgd  9880  bj-bdfindis  10072  bj-peano4  10080  strcollnfALT  10111  alsi1d  10120  alsi2d  10121  alsc1d  10122  alsc2d  10123