Theorem sylib 120

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 118	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sylbb1  135  bicomd  139  pm5.74d  180  bitri  182  3imtr3i  198  ancomd  263  pm4.71d  385  pm4.71rd  386  imdistand  435  orcomd  680  3mix3  1109  mpjao3dan  1238  ecase23d  1281  exlimdh  1527  nexd  1544  alexnim  1579  excomim  1593  19.41  1616  nfexd  1684  sbh  1699  sbcof2  1731  sbidm  1772  sb6rf  1774  nfsbt  1891  dvelimALT  1927  dvelimfv  1928  dvelimor  1935  eu2  1985  2euex  2028  eqcomd  2086  3eltr3g  2163  abbid  2195  neneqd  2266  syl5eqner  2276  3netr3g  2279  necomd  2331  r19.21bi  2449  nrexdv  2454  rexlimd  2474  rabbidva  2592  elisset  2613  euind  2779  rmoan  2790  reuind  2795  2rmorex  2796  spsbc  2826  spesbc  2899  eldifad  2984  eldifbd  2985  3sstr3g  3039  syl6sseq  3045  difindiss  3218  un00  3290  undifss  3323  ifcldcd  3381  disjpr2  3456  difprsn1  3525  diftpsn3  3527  difsnss  3531  sneqr  3552  preqr1  3560  preq12b  3562  oprcl  3594  intab  3665  riinm  3750  rintm  3765  sndisj  3781  3brtr3g  3816  trint  3890  iinexgm  3929  pwel  3973  exss  3982  0nelop  4003  euotd  4009  opelopabsb  4015  pwunim  4041  issod  4074  frind  4107  suctr  4176  orduniss  4180  onelini  4185  oneluni  4186  eusv2i  4205  rexxfrd  4213  rabxfrd  4219  reuhypd  4221  iunpw  4229  sucexg  4242  ordsucim  4244  ordtriexmidlem  4263  ordtri2or2exmidlem  4269  onsucelsucexmidlem  4272  ordsucunielexmid  4274  orddif  4290  suc11g  4300  onintexmid  4315  reg3exmidlemwe  4321  tfisi  4328  peano1  4335  peano2  4336  finds2  4342  brrelex12  4399  brel  4410  ssrel  4446  ssrel2  4448  ssrelrel  4458  elrel  4460  xpsspw  4468  relop  4504  dmxpm  4573  opelresi  4641  ndmima  4722  poirr2  4737  xpmlem  4764  xpimasn  4789  iotass  4904  iotacl  4910  dffun5r  4934  funeu  4946  funeu2  4947  funopg  4954  funun  4964  funtp  4972  funcnvuni  4988  funcnvres2  4994  imadiflem  4998  imadif  4999  funimaexglem  5002  fneu2  5024  fnimaeq0  5040  fnmpt  5045  fun2  5084  f00  5101  foimacnv  5164  resdif  5168  f1ococnv1  5175  fv3  5218  relelfvdm  5226  nfvres  5227  dffn5im  5240  mptfvex  5277  fvmptdf  5279  fvmptdv2  5281  fndmdif  5293  dff4im  5334  fmpt  5340  fmptd  5343  f1oresrab  5350  fcoconst  5355  fsn  5356  ftpg  5368  fsnunf  5383  resfunexg  5403  isores1  5474  riota2df  5508  acexmidlemcase  5527  brabvv  5571  funoprabg  5620  fnovim  5629  ovmpt2df  5652  ovi3  5657  grprinvlem  5715  grprinvd  5716  grpridd  5717  elmpt2cl  5718  1stcof  5810  2ndcof  5811  fnmpt2  5848  fmpt2co  5857  fo2ndf  5868  f1o2ndf1  5869  brtpos2  5889  reldmtpos  5891  dftpos3  5900  dftpos4  5901  tpostpos2  5903  tposf2  5906  tposf12  5907  tposfo  5909  tposf  5910  smores2  5932  tfrlem1  5946  tfrlem3-2d  5951  tfrlemisucaccv  5962  tfrlemibxssdm  5964  tfrlemibfn  5965  tfrlemi1  5969  tfrexlem  5971  rdgivallem  5991  rdgisucinc  5995  rdgon  5996  frecabex  6007  frecfnom  6009  frecsuclemdm  6011  freccl  6016  omsuc  6074  nntri2  6096  nnsseleq  6102  nndifsnid  6103  nnm00  6125  ecexr  6134  swoer  6157  elqsn0m  6197  iinerm  6201  erinxp  6203  ecinxp  6204  eroveu  6220  eroprf  6222  dom2lem  6275  fundmen  6309  nneneq  6343  fidifsnid  6356  ssfilem  6360  dif1en  6364  fin0  6369  fin0or  6370  diffitest  6371  diffisn  6377  ac6sfi  6379  onunsnss  6383  unsnfidcel  6386  suplubti  6413  supelti  6415  infmoti  6441  infisoti  6445  elni2  6504  indpi  6532  distrnqg  6577  subhalfnqq  6604  enq0sym  6622  enq0ref  6623  enq0tr  6624  nqnq0pi  6628  nnnq0lem1  6636  distrnq0  6649  elinp  6664  elnp1st2nd  6666  prltlu  6677  prnmaxl  6678  prnminu  6679  prarloc  6693  nqprm  6732  appdivnq  6753  prmuloc  6756  mullocpr  6761  distrlem4prl  6774  distrlem4pru  6775  ltexprlemm  6790  ltexprlemopl  6791  ltexprlemopu  6793  cauappcvgprlemopl  6836  cauappcvgprlemopu  6838  cauappcvgprlemdisj  6841  cauappcvgprlem2  6850  cauappcvgprlemlim  6851  caucvgprlemnkj  6856  caucvgprlemopl  6859  caucvgprlemopu  6861  caucvgprlemdisj  6864  caucvgprlemcl  6866  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlem2  6870  caucvgprprlemcbv  6877  caucvgprprlemval  6878  caucvgprprlemlol  6888  caucvgprprlemexbt  6896  caucvgprprlem1  6899  prsrlem1  6919  gt0srpr  6925  caucvgsrlemcl  6965  caucvgsrlembound  6970  caucvgsrlemgt1  6971  ltresr  7007  nnindnn  7059  axcaucvglemcl  7061  axcaucvglemval  7063  axcaucvglemcau  7064  axcaucvglemres  7065  nnind  8055  nn0supp  8340  nn0ge2m1nn  8348  zleloe  8398  zapne  8422  nn0lt2  8429  suprzclex  8445  zindd  8465  uzm1  8649  uzin  8651  elnn1uz2  8694  nn01to3  8702  divfnzn  8706  qapne  8724  xrltnsym2  8869  iooval2  8938  icoshftf1o  9013  fztri3or  9058  fzneuz  9118  4fvwrd4  9150  elfzo0  9191  ioom  9269  fzfig  9422  uzsinds  9428  iseqovex  9439  iseqval  9440  monoord2  9456  iseqdistr  9470  expivallem  9477  expival  9478  expp1  9483  expcl2lemap  9488  expclzap  9501  expap0i  9508  ibcval5  9690  cvg1nlemcau  9870  rexanuz  9874  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemsqa  9910  resqrexlemex  9911  rersqreu  9914  caubnd2  10003  maxleast  10099  fimaxre2  10109  minmax  10112  climreu  10136  iiserex  10177  climcvg1nlem  10186  serif0  10189  mod2eq1n2dvds  10279  ndvdssub  10330  infssuzex  10345  infssuzcldc  10347  gcdsupex  10349  gcdsupcl  10350  bezoutlemnewy  10385  bezoutlemmain  10387  bezoutlembi  10394  bezoutlemeu  10396  bezoutlemle  10397  nn0seqcvgd  10423  eucalgf  10437  eucalginv  10438  lcmval  10445  prmind2  10502  bj-bdfindis  10742  bj-peano4  10750  strcollnfALT  10781  alsi1d  10792  alsi2d  10793  alsc1d  10794  alsc2d  10795