Theorem sylib 121

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

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbb1  136  bicomd  140  pm5.74d  181  bitri  183  3imtr3i  199  ancomd  265  pm4.71d  388  pm4.71rd  389  imdistand  439  orcomd  689  3mix3  1120  mpjao3dan  1253  ecase23d  1296  exlimdh  1543  nexd  1560  alexnim  1595  excomim  1609  19.41  1632  equcomd  1651  nfexd  1702  sbh  1717  sbcof2  1749  sbidm  1790  sb6rf  1792  nfsbt  1910  dvelimALT  1946  dvelimfv  1947  dvelimor  1954  eu2  2004  2euex  2047  eqcomd  2105  3eltr3g  2184  abbid  2216  neneqd  2288  syl5eqner  2298  3netr3g  2301  necomd  2353  r19.21bi  2479  nrexdv  2484  rexlimd  2505  rabbidva  2629  elisset  2655  euind  2824  rmoan  2837  reuind  2842  2rmorex  2843  spsbc  2873  spesbc  2946  eldifad  3032  eldifbd  3033  3sstr3g  3089  syl6sseq  3095  difindiss  3277  un00  3356  undifss  3390  ifcldcd  3454  disjpr2  3534  difprsn1  3606  diftpsn3  3608  difsnss  3613  sneqr  3634  preqr1  3642  preq12b  3644  oprcl  3676  intab  3747  riinm  3832  rintm  3851  disjiun  3870  sndisj  3871  3brtr3g  3906  trint  3981  iinexgm  4019  exmidexmid  4060  exmid01  4061  pwel  4078  exss  4087  0nelop  4108  euotd  4114  opelopabsb  4120  pwunim  4146  issod  4179  frind  4212  suctr  4281  orduniss  4285  onelini  4290  oneluni  4291  eusv2i  4314  rexxfrd  4322  rabxfrd  4328  reuhypd  4330  iunpw  4339  sucexg  4352  ordsucim  4354  ordtriexmidlem  4373  ordtri2or2exmidlem  4379  onsucelsucexmidlem  4382  ordsucunielexmid  4384  orddif  4400  suc11g  4410  onintexmid  4425  reg3exmidlemwe  4431  tfisi  4439  peano1  4446  peano2  4447  finds2  4453  omsinds  4473  brrelex12  4515  brel  4529  ssrel  4565  ssrel2  4567  ssrelrel  4577  elrel  4579  xpsspw  4589  relop  4627  dmxpm  4697  opelresi  4766  ndmima  4852  poirr2  4867  xpmlem  4895  xpimasn  4923  iotass  5041  iotacl  5047  dffun5r  5071  funeu  5084  funeu2  5085  funfnd  5090  funopg  5093  funun  5103  funinsn  5108  funtp  5112  funcnvuni  5128  funcnvres2  5134  imadiflem  5138  imadif  5139  funimaexglem  5142  fneu2  5164  fnimaeq0  5180  fnmpt  5185  fun2  5232  f00  5250  f0bi  5251  foimacnv  5319  resdif  5323  f1ococnv1  5330  fv3  5376  relelfvdm  5385  nfvres  5386  dffn5im  5399  mptfvex  5438  fvmptdf  5440  fvmptdv2  5442  fndmdif  5457  dff4im  5498  fmpt  5502  fmptd  5506  fmptdf  5509  f1oresrab  5517  fcoconst  5523  fsn  5524  ftpg  5536  fsnunf  5552  resfunexg  5573  isores1  5647  riota2df  5682  acexmidlemcase  5701  brabvv  5749  funoprabg  5802  fnovim  5811  ovmpodf  5834  ovi3  5839  grprinvlem  5897  grprinvd  5898  grpridd  5899  elmpocl  5900  1stcof  5992  2ndcof  5993  fnmpo  6030  fmpoco  6043  fo2ndf  6054  f1o2ndf1  6055  disjxp1  6063  brtpos2  6078  reldmtpos  6080  dftpos3  6089  dftpos4  6090  tpostpos2  6092  tposf2  6095  tposf12  6096  tposfo  6098  tposf  6099  smores2  6121  tfrlem1  6135  tfrlem3-2d  6139  tfrlemisucaccv  6152  tfrlemibxssdm  6154  tfrlemibfn  6155  tfrlemi1  6159  tfrexlem  6161  tfr1onlemsucaccv  6168  tfr1onlembxssdm  6170  tfr1onlembfn  6171  tfr1onlemaccex  6175  tfrcllemsucaccv  6181  tfrcllembxssdm  6183  tfrcllembfn  6184  tfrcllemaccex  6188  tfrcldm  6190  rdgivallem  6208  rdgisucinc  6212  frecabex  6225  frecfnom  6228  frecfcllem  6231  frecsuclem  6233  omsuc  6298  nntri2  6320  nnsucuniel  6321  nnsseleq  6327  nnm00  6355  ecexr  6364  swoer  6387  elqsn0m  6427  iinerm  6431  erinxp  6433  ecinxp  6434  eroveu  6450  eroprf  6452  mapprc  6476  mapsn  6514  ixpprc  6543  ixp0  6555  resixp  6557  elixpsn  6559  dom2lem  6596  fundmen  6630  dom0  6661  xpf1o  6667  mapxpen  6671  xpmapenlem  6672  ssenen  6674  nneneq  6680  ssfilem  6698  dif1en  6702  dif1enen  6703  fin0  6708  fin0or  6709  diffitest  6710  diffisn  6716  ac6sfi  6721  fimax2gtrilemstep  6723  fimax2gtri  6724  finexdc  6725  onunsnss  6734  unsnfidcel  6738  undifdcss  6740  undifdc  6741  fiintim  6746  fisseneq  6749  fidcenumlemr  6771  sbthlemi4  6776  sbthlemi5  6777  sbthlemi9  6781  suplubti  6802  supelti  6804  infmoti  6830  infisoti  6834  djulclb  6855  updjud  6882  omp1eomlem  6894  0ct  6907  ctmlemr  6908  ctssdclemn0  6910  ctssdclemr  6911  ctssdc  6912  enumct  6914  finomni  6924  fodjuomnilemdc  6928  fodjum  6930  fodjuomnilemres  6932  fodjumkvlemres  6944  en2eleq  6960  exmidfodomrlemeldju  6964  exmidfodomrlemreseldju  6965  exmidfodomrlemim  6966  elni2  7023  indpi  7051  distrnqg  7096  subhalfnqq  7123  enq0sym  7141  enq0ref  7142  enq0tr  7143  nqnq0pi  7147  nnnq0lem1  7155  distrnq0  7168  elinp  7183  elnp1st2nd  7185  prltlu  7196  prnmaxl  7197  prnminu  7198  prarloc  7212  nqprm  7251  appdivnq  7272  prmuloc  7275  mullocpr  7280  distrlem4prl  7293  distrlem4pru  7294  ltexprlemm  7309  ltexprlemopl  7310  ltexprlemopu  7312  cauappcvgprlemopl  7355  cauappcvgprlemopu  7357  cauappcvgprlemdisj  7360  cauappcvgprlem2  7369  cauappcvgprlemlim  7370  caucvgprlemnkj  7375  caucvgprlemopl  7378  caucvgprlemopu  7380  caucvgprlemdisj  7383  caucvgprlemcl  7385  caucvgprlemladdfu  7386  caucvgprlemladdrl  7387  caucvgprlem2  7389  caucvgprprlemcbv  7396  caucvgprprlemval  7397  caucvgprprlemlol  7407  caucvgprprlemexbt  7415  caucvgprprlem1  7418  prsrlem1  7438  gt0srpr  7444  caucvgsrlemcl  7484  caucvgsrlembound  7489  caucvgsrlemgt1  7490  ltresr  7526  nnindnn  7578  axcaucvglemcl  7580  axcaucvglemval  7582  axcaucvglemcau  7583  axcaucvglemres  7584  sup3exmid  8573  nnind  8594  nn0supp  8881  nn0ge2m1nn  8889  zleloe  8953  zapne  8977  nn0lt2  8984  suprzclex  9001  zindd  9021  uzm1  9206  uzin  9208  elnn1uz2  9251  nn01to3  9259  divfnzn  9263  qapne  9281  xrltnsym2  9421  xaddass  9493  xleadd1a  9497  xlt2add  9504  xlesubadd  9507  iooval2  9539  icoshftf1o  9615  fztri3or  9660  fzneuz  9722  4fvwrd4  9758  elfzo0  9800  exbtwnzlemex  9868  ioom  9879  fzfig  10044  uzennn  10050  uzsinds  10056  iseqovex  10070  seq3val  10072  seqvalcd  10073  seqf  10075  seqovcd  10077  monoord2  10091  iseqf1olemjpcl  10109  iseqf1olemqpcl  10110  seq3f1olemqsum  10114  seq3f1o  10118  seq3distr  10127  expp1  10141  expcl2lemap  10146  expclzap  10159  expap0i  10166  bcval5  10350  hashinfuni  10364  hashennnuni  10366  hashnncl  10383  resunimafz0  10415  zfz1isolemiso  10423  zfz1isolem1  10424  zfz1iso  10425  seq3shft  10451  cvg1nlemcau  10596  rexanuz  10600  resqrexlemoverl  10633  resqrexlemglsq  10634  resqrexlemsqa  10636  resqrexlemex  10637  rersqreu  10640  caubnd2  10729  maxleast  10825  fimaxre2  10837  minmax  10840  xrmaxiflemcl  10853  xrmaxiflemab  10855  xrmaxiflemlub  10856  xrmaxadd  10869  xrminmax  10873  xrbdtri  10884  climreu  10905  reccn2ap  10921  iserex  10947  climcvg1nlem  10957  serf0  10960  fz1f1o  10983  summodclem3  10988  zsumdc  10992  fsum3  10995  isumz  10997  isumss  10999  isumss2  11001  fsumsersdc  11003  fsum3ser  11005  fsumsplit  11015  isumclim2  11030  isumclim3  11031  fsum2dlemstep  11042  fsumcnv  11045  fisumcom2  11046  bcxmas  11097  isumle  11103  cvgratnnlemnexp  11132  cvgratnnlemmn  11133  cvgratz  11140  mertenslemub  11142  mertenslemi1  11143  mertenslem2  11144  mertensabs  11145  ef0lem  11164  mod2eq1n2dvds  11371  ndvdssub  11422  infssuzex  11437  infssuzcldc  11439  gcdsupex  11441  gcdsupcl  11442  bezoutlemnewy  11477  bezoutlemmain  11479  bezoutlembi  11486  bezoutlemeu  11488  bezoutlemle  11489  nn0seqcvgd  11515  eucalgf  11529  eucalginv  11530  lcmval  11537  prmind2  11594  dfphi2  11688  phiprmpw  11690  phimullem  11693  ennnfonelemom  11713  ennnfoneleminc  11716  ennnfonelemhf1o  11718  ennnfonelemex  11719  ennnfonelemhom  11720  ennnfonelemdm  11725  ennnfonelemr  11728  ennnfonelemim  11729  exmidunben  11731  ctinfom  11733  inffinp1  11734  ctinf  11735  structcnvcnv  11757  setscom  11781  restid2  11911  topontopon  11969  eltg3i  12007  epttop  12041  difopn  12059  uncld  12064  0nnei  12104  resttopon  12122  restabs  12126  restopnb  12132  lmcvg  12167  cnptopco  12172  cnss1  12176  cnss2  12177  cncnpi  12178  cncnp2m  12181  cnrest  12185  cnrest2  12186  cnrest2r  12187  cnptoprest  12189  cnptoprest2  12190  lmss  12196  lmff  12199  lmtopcnp  12200  lmcn  12201  txbasval  12217  upxp  12222  txcnmpt  12223  txdis1cn  12228  txlm  12229  lmcn2  12230  cnmpt11  12233  cnmpt11f  12234  cnmpt1t  12235  cnmpt12  12237  cnmpt21  12241  cnmpt21f  12242  cnmpt2t  12243  cnmpt22  12244  cnmpt22f  12245  cnmptcom  12248  isxmet2d  12276  blfvalps  12313  xblss2ps  12332  xblss2  12333  blfps  12337  blf  12338  unirnblps  12350  unirnbl  12351  isxms2  12380  bdxmet  12429  bdmet  12430  blssioo  12464  tgioo  12465  mulcncflem  12502  limcrcl  12509  bj-bdfindis  12730  bj-peano4  12738  strcollnfALT  12769  pwtrufal  12777  pwntru  12778  pwf1oexmid  12780  nnsf  12783  nninfalllem1  12787  nninfall  12788  nninfsellemqall  12795  exmidsbthrlem  12801  sbthom  12805  cvgcmp2nlemabs  12811  trilpo  12820  alsi1d  12829  alsi2d  12830  alsc1d  12831  alsc2d  12832