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-mp 5  ax-1 6  ax-2 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  390  pm4.71rd  391  imdistand  443  orcomd  718  3mix3  1152  mpjao3dan  1285  ecase23d  1328  exlimdh  1575  nexd  1592  alexnim  1627  excomim  1641  19.41  1664  equcomd  1683  nfexd  1734  sbh  1749  sbcof2  1782  sbidm  1823  sb6rf  1825  nfsbt  1949  dvelimALT  1985  dvelimfv  1986  dvelimor  1993  eu2  2043  2euex  2086  eqcomd  2145  3eltr3g  2224  abbid  2256  neneqd  2329  eqnetrrid  2339  3netr3g  2342  necomd  2394  r19.21bi  2520  nrexdv  2525  rexlimd  2546  rabbidva  2674  elisset  2700  euind  2871  rmoan  2884  reuind  2889  2rmorex  2890  spsbc  2920  spesbc  2994  eldifad  3082  eldifbd  3083  3sstr3g  3139  sseqtrdi  3145  difindiss  3330  un00  3409  undifss  3443  ifcldcd  3507  disjpr2  3587  difprsn1  3659  diftpsn3  3661  difsnss  3666  sneqr  3687  preqr1  3695  preq12b  3697  oprcl  3729  intab  3800  riinm  3885  rintm  3905  disjiun  3924  sndisj  3925  3brtr3g  3961  trint  4041  iinexgm  4079  exmidexmid  4120  exmid01  4121  pwntru  4122  pwel  4140  exss  4149  0nelop  4170  euotd  4176  opelopabsb  4182  pwunim  4208  issod  4241  frind  4274  suctr  4343  orduniss  4347  onelini  4352  oneluni  4353  eusv2i  4376  rexxfrd  4384  rabxfrd  4390  reuhypd  4392  iunpw  4401  sucexg  4414  ordsucim  4416  ordtriexmidlem  4435  ordtri2or2exmidlem  4441  onsucelsucexmidlem  4444  ordsucunielexmid  4446  orddif  4462  suc11g  4472  onintexmid  4487  reg3exmidlemwe  4493  tfisi  4501  peano1  4508  peano2  4509  finds2  4515  omsinds  4535  brrelex12  4577  brel  4591  ssrel  4627  ssrel2  4629  ssrelrel  4639  elrel  4641  xpsspw  4651  relop  4689  dmxpm  4759  opelresi  4830  ndmima  4916  poirr2  4931  xpmlem  4959  xpimasn  4987  iotass  5105  iotacl  5111  dffun5r  5135  funeu  5148  funeu2  5149  funfnd  5154  funopg  5157  funun  5167  funinsn  5172  funtp  5176  funcnvuni  5192  funcnvres2  5198  imadiflem  5202  imadif  5203  funimaexglem  5206  fneu2  5228  fnimaeq0  5244  fnmpt  5249  fun2  5296  f00  5314  f0bi  5315  foimacnv  5385  resdif  5389  f1ococnv1  5396  fv3  5444  relelfvdm  5453  nfvres  5454  dffn5im  5467  mptfvex  5506  fvmptdf  5508  fvmptdv2  5510  fndmdif  5525  dff4im  5566  fmpt  5570  fmptd  5574  fmptdf  5577  f1oresrab  5585  fcoconst  5591  fsn  5592  ftpg  5604  fsnunf  5620  resfunexg  5641  isores1  5715  riota2df  5750  acexmidlemcase  5769  brabvv  5817  funoprabg  5870  fnovim  5879  ovmpodf  5902  ovi3  5907  grprinvlem  5965  grprinvd  5966  grpridd  5967  elmpocl  5968  1stcof  6061  2ndcof  6062  fnmpo  6100  fmpoco  6113  fo2ndf  6124  f1o2ndf1  6125  disjxp1  6133  brtpos2  6148  reldmtpos  6150  dftpos3  6159  dftpos4  6160  tpostpos2  6162  tposf2  6165  tposf12  6166  tposfo  6168  tposf  6169  smores2  6191  tfrlem1  6205  tfrlem3-2d  6209  tfrlemisucaccv  6222  tfrlemibxssdm  6224  tfrlemibfn  6225  tfrlemi1  6229  tfrexlem  6231  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemaccex  6245  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemaccex  6258  tfrcldm  6260  rdgivallem  6278  rdgisucinc  6282  frecabex  6295  frecfnom  6298  frecfcllem  6301  frecsuclem  6303  omsuc  6368  nntri2  6390  nnsucuniel  6391  nnsseleq  6397  nnm00  6425  ecexr  6434  swoer  6457  elqsn0m  6497  iinerm  6501  erinxp  6503  ecinxp  6504  eroveu  6520  eroprf  6522  mapprc  6546  mapsn  6584  ixpprc  6613  ixp0  6625  resixp  6627  elixpsn  6629  dom2lem  6666  fundmen  6700  dom0  6732  xpf1o  6738  mapxpen  6742  xpmapenlem  6743  ssenen  6745  nneneq  6751  ssfilem  6769  dif1en  6773  dif1enen  6774  fin0  6779  fin0or  6780  diffitest  6781  diffisn  6787  ac6sfi  6792  fimax2gtrilemstep  6794  fimax2gtri  6795  finexdc  6796  onunsnss  6805  unsnfidcel  6809  undifdcss  6811  undifdc  6812  fiintim  6817  fisseneq  6820  fidcenumlemr  6843  sbthlemi4  6848  sbthlemi5  6849  sbthlemi9  6853  fifo  6868  suplubti  6887  supelti  6889  infmoti  6915  infisoti  6919  djulclb  6940  updjud  6967  omp1eomlem  6979  0ct  6992  ctmlemr  6993  ctssdclemn0  6995  ctssdccl  6996  ctssdc  6998  enumct  7000  finomni  7012  fodjuomnilemdc  7016  fodjum  7018  fodjuomnilemres  7020  fodjumkvlemres  7033  exmidonfinlem  7049  en2eleq  7051  exmidfodomrlemeldju  7055  exmidfodomrlemreseldju  7056  exmidfodomrlemim  7057  acfun  7063  exmidaclem  7064  ccfunen  7079  elni2  7122  indpi  7150  distrnqg  7195  subhalfnqq  7222  enq0sym  7240  enq0ref  7241  enq0tr  7242  nqnq0pi  7246  nnnq0lem1  7254  distrnq0  7267  elinp  7282  elnp1st2nd  7284  prltlu  7295  prnmaxl  7296  prnminu  7297  prarloc  7311  nqprm  7350  appdivnq  7371  prmuloc  7374  mullocpr  7379  distrlem4prl  7392  distrlem4pru  7393  ltexprlemm  7408  ltexprlemopl  7409  ltexprlemopu  7411  cauappcvgprlemopl  7454  cauappcvgprlemopu  7456  cauappcvgprlemdisj  7459  cauappcvgprlem2  7468  cauappcvgprlemlim  7469  caucvgprlemnkj  7474  caucvgprlemopl  7477  caucvgprlemopu  7479  caucvgprlemdisj  7482  caucvgprlemcl  7484  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  caucvgprlem2  7488  caucvgprprlemcbv  7495  caucvgprprlemval  7496  caucvgprprlemlol  7506  caucvgprprlemexbt  7514  caucvgprprlem1  7517  suplocexprlemrl  7525  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemdisj  7528  suplocexprlemloc  7529  suplocexprlemub  7531  suplocexprlemlub  7532  prsrlem1  7550  gt0srpr  7556  caucvgsrlemcl  7597  caucvgsrlembound  7602  caucvgsrlemgt1  7603  suplocsrlemb  7614  suplocsrlem  7616  suplocsr  7617  ltresr  7647  nnindnn  7701  axcaucvglemcl  7703  axcaucvglemval  7705  axcaucvglemcau  7706  axcaucvglemres  7707  axpre-suploclemres  7709  axpre-suploc  7710  sup3exmid  8715  nnind  8736  nn0supp  9029  nn0ge2m1nn  9037  zleloe  9101  zapne  9125  nn0lt2  9132  suprzclex  9149  zindd  9169  uzm1  9356  uzin  9358  elnn1uz2  9401  nn01to3  9409  divfnzn  9413  qapne  9431  xrltnsym2  9580  xaddass  9652  xleadd1a  9656  xlt2add  9663  xlesubadd  9666  iooval2  9698  icoshftf1o  9774  fztri3or  9819  fzneuz  9881  4fvwrd4  9917  elfzo0  9959  exbtwnzlemex  10027  ioom  10038  fzfig  10203  uzennn  10209  uzsinds  10215  iseqovex  10229  seq3val  10231  seqvalcd  10232  seqf  10234  seqovcd  10236  monoord2  10250  iseqf1olemjpcl  10268  iseqf1olemqpcl  10269  seq3f1olemqsum  10273  seq3f1o  10277  seq3distr  10286  expp1  10300  expcl2lemap  10305  expclzap  10318  expap0i  10325  bcval5  10509  hashinfuni  10523  hashennnuni  10525  hashnncl  10542  resunimafz0  10574  zfz1isolemiso  10582  zfz1isolem1  10583  zfz1iso  10584  seq3shft  10610  cvg1nlemcau  10756  rexanuz  10760  resqrexlemoverl  10793  resqrexlemglsq  10794  resqrexlemsqa  10796  resqrexlemex  10797  rersqreu  10800  caubnd2  10889  maxleast  10985  fimaxre2  10998  minmax  11001  xrmaxiflemcl  11014  xrmaxiflemab  11016  xrmaxiflemlub  11017  xrmaxadd  11030  xrminmax  11034  xrbdtri  11045  climreu  11066  reccn2ap  11082  iserex  11108  climcvg1nlem  11118  serf0  11121  fz1f1o  11144  summodclem3  11149  zsumdc  11153  fsum3  11156  isumz  11158  isumss  11160  isumss2  11162  fsumsersdc  11164  fsum3ser  11166  fsumsplit  11176  isumclim2  11191  isumclim3  11192  fsum2dlemstep  11203  fsumcnv  11206  fisumcom2  11207  bcxmas  11258  isumle  11264  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  cvgratz  11301  mertenslemub  11303  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  ef0lem  11366  mod2eq1n2dvds  11576  ndvdssub  11627  infssuzex  11642  infssuzcldc  11644  gcdsupex  11646  gcdsupcl  11647  bezoutlemnewy  11684  bezoutlemmain  11686  bezoutlembi  11693  bezoutlemeu  11695  bezoutlemle  11696  nn0seqcvgd  11722  eucalgf  11736  eucalginv  11737  lcmval  11744  prmind2  11801  dfphi2  11896  phiprmpw  11898  phimullem  11901  ennnfonelemom  11921  ennnfoneleminc  11924  ennnfonelemhf1o  11926  ennnfonelemex  11927  ennnfonelemhom  11928  ennnfonelemdm  11933  ennnfonelemr  11936  ennnfonelemim  11937  exmidunben  11939  ctinfom  11941  inffinp1  11942  ctinf  11943  enctlem  11945  ctiunctlemu1st  11947  ctiunctlemu2nd  11948  ctiunctlemudc  11950  ctiunct  11953  unct  11954  structcnvcnv  11975  setscom  11999  restid2  12129  topontopon  12187  eltg3i  12225  epttop  12259  difopn  12277  uncld  12282  0nnei  12322  resttopon  12340  restabs  12344  restopnb  12350  lmcvg  12386  cnptopco  12391  cnss1  12395  cnss2  12396  cncnpi  12397  cncnp2m  12400  cnrest  12404  cnrest2  12405  cnrest2r  12406  cnptoprest  12408  cnptoprest2  12409  lmss  12415  lmff  12418  lmtopcnp  12419  lmcn  12420  txbasval  12436  upxp  12441  txcnmpt  12442  txdis1cn  12447  txlm  12448  lmcn2  12449  cnmpt11  12452  cnmpt11f  12453  cnmpt1t  12454  cnmpt12  12456  cnmpt21  12460  cnmpt21f  12461  cnmpt2t  12462  cnmpt22  12463  cnmpt22f  12464  cnmptcom  12467  hmeocnv  12476  hmeof1o  12478  hmeores  12484  txhmeo  12488  txswaphmeo  12490  isxmet2d  12517  blfvalps  12554  xblss2ps  12573  xblss2  12574  blfps  12578  blf  12579  unirnblps  12591  unirnbl  12592  isxms2  12621  bdxmet  12670  bdmet  12671  xmetxp  12676  xmettx  12679  blssioo  12714  tgioo  12715  mulcncflem  12759  dedekindeulemuub  12764  dedekindeulemub  12765  dedekindeulemloc  12766  dedekindeulemlu  12768  suplociccreex  12771  suplociccex  12772  dedekindicclemuub  12773  dedekindicclemub  12774  dedekindicclemloc  12775  dedekindicclemlu  12777  dedekindicc  12780  ivthinclemlopn  12783  ivthinclemuopn  12785  limcrcl  12796  limcmpted  12801  limccnp2lem  12814  limccnp2cntop  12815  limccoap  12816  dvrecap  12846  cosordlem  12930  bj-stand  12956  bj-bdfindis  13145  bj-peano4  13153  strcollnfALT  13184  pwtrufal  13192  pwf1oexmid  13194  exmid1stab  13195  subctctexmid  13196  nnsf  13199  nninfalllem1  13203  nninfall  13204  nninfsellemqall  13211  exmidsbthrlem  13217  sbthom  13221  cvgcmp2nlemabs  13227  trilpo  13236  taupi  13239  alsi1d  13247  alsi2d  13248  alsc1d  13249  alsc2d  13250