Theorem sylib 196

Description: A mixed syllogism inference from an implication and a biconditional.

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 149	. 2 ⊢ (ψ → χ)
4	1, 3	syl 10	1 ⊢ (φ → χ)

Syntax hints:   → wi 3   ↔ wb 144

This theorem is referenced by:  3imtr3i 216  ord 230  exp3a 374  imdistand 447  bicomd 524  pm2.85 582  pm5.74d 588  mpbidi 592  notbid 614  pm4.71rd 642  pm5.32d 650  pm5.18 663  ecase2d 756  consensus 772  3mix3 823  ecase23d 929  nic-ax 969  excomim 1081  19.23ai 1100  19.23ad 1102  nexd 1138  sbf 1223  hbs1f 1226  sbied 1232  sbequi 1265  sbn 1268  a4sbe 1280  a4sbim 1281  a4sbbi 1282  sb6rf 1298  sb8 1299  sb9i 1301  eu2 1435  mooran1 1464  euor2 1477  2eu1 1489  eqcomd 1523  necon2bi 1655  necon2i 1656  necon4i 1669  necomd 1683  r19.21bi 1771  nrexdv 1776  elex 1865  ceqsalg 1871  cla4gf 1906  3sstr3g 2153  syl6ss 2159  sseq0 2357  un00 2359  npss0 2362  disjpss 2372  ssnelpss 2383  pssnel 2384  difsnid 2531  sneqr 2542  preqr1 2546  preq12b 2548  reucl 2584  ssiun 2660  iununi 2686  3brtr3g 2719  axrep1 2768  axrep2 2769  axrep4 2771  axrep5 2772  class2set 2808  0inp0 2812  pwel 2838  exss 2847  opth1 2862  opthwiener 2884  pwssun 2905  sotric 2939  efrn2lp 2958  wecmpep 2968  wereu 2972  ordtri3or 3007  ordtri1 3008  ordtri3 3011  suctr 3055  ordnbtwn 3062  orddif 3065  orduniss 3066  ordtri2or 3067  suc11 3073  onelini 3081  oneluni 3082  on0eqel 3087  difex2 3101  euuni 3105  reuxfr2 3126  reuhyp 3128  iunpw 3137  epne3 3139  dfwe2 3140  ordeleqon 3144  sucexg 3167  suceloni 3170  ordunisuc 3186  onuninsuci 3194  ordunisuc2 3198  dflim3 3201  limsssuc 3204  tfi 3207  tfindsg2 3214  find 3243  finds2 3246  ssrel 3334  ssrelrel 3340  elrel 3342  xpsspw 3346  relop 3365  opelxpex2 3369  dmxp 3419  resopab2 3488  relimasn 3517  ndmima 3526  funopg 3652  funun 3659  funcnvuni 3669  funin 3671  funcnvres2 3675  imadif 3679  fneu2 3699  fn0 3711  fnopabg 3722  fcoi2 3753  fcnvres 3755  f00 3764  foconst 3791  foimacnv 3814  resdif 3816  resin 3817  f1ococnv2 3819  f1ococnv1 3820  fvprc 3832  fv3 3844  tz6.12-2 3850  fvopabn 3897  elrnopabg 3914  exfo 3936  fopab2 3937  fsn 3948  fnressn 3951  funoprabg 4070  1stcof 4160  elrnoprabg 4186  curry1 4193  curry1f 4194  curry2 4196  curry2f 4197  onopriun 4211  tfrlem5 4216  tfrlem8 4219  tz7.48-2 4258  abianfp 4263  oalimcl 4330  omlimcl 4345  brecop2 4448  ecopoprdm 4450  mapsn 4486  ixp0 4502  en2d 4541  dom2d 4545  fundmen 4569  unen 4575  pw2en 4587  ac6sfilem3 4590  sbthlem3 4594  sbthlem4 4595  sbthlem5 4596  sbthlem6 4597  sdomdomtr 4614  fodomr 4628  xpen 4635  mapenlem2 4637  mapdom2 4641  mapxpen 4642  xpmapenlem3 4645  xpmapenlem5 4647  mapunen 4649  pwen 4650  ssenen 4651  nneneq 4659  php 4660  isfinite1 4677  infn0 4679  ssfi 4683  unblem2 4687  isfinite2 4692  unfi 4697  unifi 4701  fiint 4703  abfii2 4705  pwfilem 4713  zfregcl 4738  elirrv 4741  inf3lem3 4760  inf3lem6 4763  infeq5 4766  noinfep 4786  zfregs 4793  r1val1 4804  rankr1 4820  rankuni 4844  rankval4 4848  rankc2 4852  rankelun 4853  rankelpr 4854  rankelop 4855  rankxplim 4858  rankxplim3 4860  rankxpsuc 4861  hta 4874  aceq3lem 4878  aceq5lem4 4884  aceq5 4886  ac6lem 4900  ac9s 4910  kmlem1 4911  kmlem4 4914  kmlem5 4915  kmlem7 4917  kmlem11 4921  zorn2lem4 4937  zorn2lem6 4939  zorn 4943  fodomb 4946  brdom3 4947  brdom5 4948  brdom4 4949  imadomg 4952  ficardom 4977  cardmin 5010  cardprc 5011  alephnbtwn 5018  cardaleph 5035  alephval3 5053  cflem 5055  cfval 5056  cfeq0 5064  cdaval 5069  nd1 5092  nd2 5093  axpownd 5107  zfcndext 5119  zfcndrep 5120  distrpq 5221  prn0 5247  prnmax 5253  genpn0 5260  genpnnp 5262  prlem934 5293  ltaddpr 5294  prlem936 5309  reclem2pr 5311  suplem1pr 5315  suppsr 5376  supsrlem6 5384  ltresr 5412  supre 5414  negeui 5509  lttri4 5669  ltnsym2 5687  renfdisj 5693  xrltnsym2 5705  xrrebnd 5722  receui 5853  rec11ii 5916  eqnegi 5944  nnind 6082  nn1suc 6084  nnleltp1 6100  nominpos 6189  lble 6215  bndndx 6241  xrsupsslem 6244  xrinfmsslem 6245  xrsupss 6246  xrinfmss 6247  supxrre 6251  elnnz 6313  elnnz1 6323  uzwo3 6390  icounlem 6539  snunioolem 6541  uzwo 6582  uzwoOLD 6583  nnwof 6586  elfzp1 6641  fzneuz 6649  expnnval 6767  discrlem3 6859  nn0opthlem2 6866  nn0opthi 6867  sqrlem13 6886  sqr2irrlem3 6927  crulem 6937  crne0i 6940  creui 6944  replim 6962  abssubne0 7085  cvg1 7124  cvg2i 7125  cvg3i 7126  faclbnd4lem4 7154  dffsum 7201  serzfsum 7207  fsump1s 7216  fsum1ps 7221  fsumshft 7234  fsumcmp 7243  bcxmas 7279  clm3i 7282  climreu 7304  climrecl 7313  climge0 7315  climubii 7356  dfisum 7395  infcvglem1 7425  infcvglem3 7427  cvgratlem5 7459  fsum0diag4 7466  cncffvrn 7478  abscncflem 7479  mulc1cncf 7484  ivthlem3 7488  ivthlem5 7490  ivthlem6 7491  ivthlem7 7492  efseq0ex 7516  efcl 7517  efcvg 7519  efcvgfsum 7520  reeftlcl 7585  eflti 7614  efcnlem1 7627  efcn 7631  sinbnd 7674  cosbnd 7675  acdc5lem1 7703  acdcALT 7708  unbenlem 7716  infxpidmlem7 7770  infxpidmlem8 7771  infxpidmlem10 7773  infxpidmlem11 7774  infxpidmlem12 7775  infpss 7786  iunctb 7787  basgen2 7851  subbas 7856  cctop 7862  clsval 7887  uncld 7891  ntrval2 7896  cmclsopn 7903  cmntrcld 7904  elcls 7914  neif 7925  0nnei 7936  islp2 7957  clslp 7958  qdensere 7961  idcn 7976  ismsg 8010  metreslem 8032  blf 8054  cncfmet 8116  lmuni 8162  lmsslem 8163  lmfexlem1 8167  metcnp4 8181  xplmi 8184  xpcn 8187  oprcn 8188  bopcnlem1 8192  bopcnlem4 8195  bcthlem4 8213  bcthlem7 8216  bcthlem9 8218  bcthlem14 8223  bcthlem28 8237  bcthlem29 8238  bcthlem30 8239  bcthlem31 8240  bcthlem33 8242  grpideu 8266  grprn 8269  isgrp2i 8293  grpinvf 8297  grpdivf 8303  gxpval 8315  gxnval 8316  resgrprn 8336  grplactf1o 8339  vcex 8446  nvvcop 8460  nvvop 8475  nvex 8477  nvmf 8513  vacnlem6 8587  sqcn 8589  va1cnlem 8599  ipf 8620  ip1cnilem2 8628  ip1cnilem3 8629  nmlno0lem 8708  siilem1 8767  ipblnfi 8772  ubthlem3 8789  minveclem26 8830  pilem1 8938  pilem2 8939  sinperlem2 8954  sincosq2sgn 8972  sincosq4sgn 8974  efifolem2 8995  efif1lem5 9006  efif1lem7 9008  grothinf 9053  axhcompl 9143  bcseqi 9262  chcmhi 9389  norm1exi 9398  shorth 9444  occllem4 9452  projlem24 9485  pjthlem11 9505  pjtheu2i 9526  pjoc1i 9540  spanval 9575  hsupval2 9576  shlej1i 9624  shs00i 9649  chj00i 9686  chabs2 9716  h1de2i 9752  cmbr4i 9820  spansnm0i 9873  nonbooli 9874  5oalem5 9881  pjssmii 9904  pjvec 9919  pjocvec 9920  hoaddcl 9964  homulcl 9965  eigposi 10042  dmadjop 10100  brafn 10151  kbop 10157  nmlnop0iALT 10199  lnopeq0i 10211  nmcopexlem4 10233  nmcfnexlem4 10262  cnlnadjlem2 10280  cnlnadjlem3 10281  cnlnadjlem4 10282  cnlnadjlem5 10283  cnlnssadj 10292  nmopcoi 10307  cnvbraval 10323  kbass2 10330  pjss1coi 10371  pjss2coi 10372  pjorthcoi 10377  pjscji 10378  pjssdif2i 10382  pjssdif1i 10383  pjclem4 10408  pjci 10409  pj3si 10416  pj3cor1i 10418  strlem3a 10460  strlem6 10464  hstrlem3a 10468  hstrlem6 10472  mdbr3 10505  mdbr4 10506  dmdbr5 10516  ssmd2 10520  mdslj1i 10527  mdslj2i 10528  mdsl2bi 10531  cvmdi 10532  mdslmd1lem1 10533  mdslmd1lem2 10534  hatomistici 10570  chrelat2i 10573  atssma 10587  atoml2i 10592  irredlem1 10599  irredlem2 10600  mdsymlem1 10612  mdsymlem2 10613  mdsymlem5 10616  dmdbr4ati 10630  dmdbr5ati 10631  ghomfo 10676  ghomgsg 10680  ghomf1olem 10681  cayleylem2 10695  eltids 10771  imfstnrelc 10810  domncnt 10872  ranncnt 10873  tostos 10883  clsint 11010  cnvhmpha 11031  hmphsyma 11034  hmphre 11036  hmeogrp 11044  homcard 11045  fipfil2 11077  efilcp 11083  filint2 11084  fgsb2 11086  efilcp2 11087  cnfilca 11088  dtt2 11110  trdom 11158  cnvtr 11161  homib 11251  ancomd 11339  ecase13d 11391  ioodisj 11413  basmetres 11416  elfiun 11421  inficlALT 11424  finsschain 11425  ordiso 11426  ordtypelem4 11430  ordtypelem6 11432  ordtypelem7 11433  hartog 11436  omsubsdomlem2 11441  infenomsub 11450  opncldf1 11454  opncldf3 11456  ntrcmp 11458  clscmp 11459  topbnd 11460  opnbnd 11461  ntrin 11463  clsun 11465  neiin 11470  subspid 11478  subcls 11481  subntr 11482  cnsubsp 11483  compsub 11488  cptclsscpt 11489  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  alexsub 11500  subtopmetlem 11505  reconnlem1 11507  reconnlem5 11511  reconn 11512  ivthALT 11515  2ndcctbss 11539  locfincomp 11575  comppfsc 11578  neibastop1 11579  neibastop2lem3 11582  neibastop2lem4 11583  topmeet 11587  fnemeet1 11589  ist1-2 11603  fbasfip 11627  opnfbas 11629  fbunfip 11631  fgfil 11638  extbas1 11641  extbas2 11642  filrn 11643  filfinnfr 11646  filssufillem 11655  ufileu 11658  filufint 11659  uffixfr 11660  uffinfix 11662  ufinffr 11663  ufilen 11664  filcon 11665  ufcondr 11666  flimcls 11684  elfilmap 11690  rnelfmlem 11698  rnelfm 11699  fmfnfmlem2 11701  fmfnfm 11704  fcluscf 11724  fclsfnflim 11726  flimfnfcls 11727  fcluscomp 11733  dirtr 11753  tailf 11756  tailmap 11759  filnetlem1 11763  filnetlem3 11765  filnetlem5 11767  filnet 11768  ssga 11777  gapm 11784  difin2 11791  oprabopabf 11807  resoprab2 11809  fnopabco 11810  upxp 11822  upixp 11823  abrexdom 11826  fimax 11837  indexa 11845  indexf 11847  fzm1 11867  sdclem1 11875  sdc 11877  seqpo 11878  incsequz 11879  incsequz2 11880  nnubfi 11881  nninfnub 11882  fsum00 11883  fsumltisumii 11885  metf1o 11907  metsstop 11909  mettrifi 11912  geomcau 11914  lmclim2 11915  metdcn 11918  addccncf 11945  sub1cncf 11946  sub2cncf 11947  cnimass 11949  cnresima 11952  cnss 11953  hmeocnv 11959  uptx 11978  txcnopab 11980  sstotbnd 11992  isbnd3 11997  heiborlem1 12011  heiborlem11 12021  heiborlem16 12026  heiborlem23 12033  heiborlem31 12041  heiborlem32 12042  heiborlem33 12043  heiborlem35 12045  heiborlem41 12051  bfplem8 12061  rrnmet 12072  rrncms 12075  rrntotbndlem1 12076  rrntotbndlem2 12077  rrntotbnd 12078  iccbnd 12082  hgrablkne0 12199

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145

Copyright terms: Public domain