Theorem sylib 198

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

Hypotheses

Ref	Expression
sylib.1	|- (ph -> ps)
sylib.2	|- (ps <-> ch)

Assertion

Ref	Expression
sylib	|- (ph -> ch)

Proof of Theorem sylib

Step	Hyp	Ref	Expression
1		sylib.1	. 2 |- (ph -> ps)
2		sylib.2	. . 3 |- (ps <-> ch)
3	2	biimp 151	. 2 |- (ps -> ch)
4	1, 3	syl 10	1 |- (ph -> ch)

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  3imtr3 218  ord 232  exp3a 375  imdistand 445  bicomd 519  pm2.85 577  pm5.74d 583  mpbidi 587  negbid 609  pm4.71rd 637  pm5.32d 645  pm5.18 657  ecase2d 748  consensus 764  3mix3 814  ecase23d 918  excomim 1021  19.23ai 1040  19.23ad 1042  nexd 1078  sbf 1169  hbs1f 1172  sbied 1178  sbequi 1212  sbn 1215  sbea4 1227  sbia4 1228  sbba4 1229  sb6rf 1244  sb8 1245  sb9i 1247  eu2 1373  mooran1 1402  euor2 1414  2eu1 1426  eqcomd 1456  necon2bi 1588  necon2i 1589  necon4i 1601  necomd 1613  r19.21bi 1701  nrexdv 1706  elex 1794  ceqsalg 1800  cla4gf 1835  3sstr3g 2072  syl6ss 2078  sseq0 2275  un00 2277  npss0 2280  disjpss 2290  ssnelpss 2301  pssnel 2302  difsnid 2437  sneqr 2447  preqr1 2451  preq12b 2453  ssiun 2560  iununi 2584  3brtr3g 2614  axrep1 2662  axrep2 2663  axrep4 2665  axrep5 2666  class2set 2702  0inp0 2706  pwel 2727  exss 2737  opth 2754  opthwiener 2770  pwssun 2789  sotric 2824  difex2 2840  euuni 2844  reucl 2848  reuxfr2 2866  reuhyp 2868  iunpw 2877  efrn2lp 2892  epne3 2893  dfwe2 2898  wecmpep 2904  wereu 2908  ordtri3or 2942  ordtri1 2943  ordtri3 2946  ordeleqon 2953  sucexg 3012  suceloni 3025  ordnbtwn 3026  orddif 3038  orduniss 3039  ordtri2or 3040  ordunisuc 3052  suc11 3056  onelin 3066  onelun 3067  onuninsuc 3071  ordunisuc2 3078  dflim3 3081  limsssuc 3084  on0eqelt 3087  tfi 3089  find 3118  finds2 3121  tfindsg2 3126  ssrel 3209  elrel 3215  xpsspw 3219  dmxp 3291  resopab2 3349  relimasn 3376  ndmima 3385  relfld 3457  funun 3494  funcnvuni 3504  funin 3506  funcnvres2 3510  imadif 3514  fneu2 3533  fn0 3545  fnopabg 3555  fcoi2 3585  fcnvres 3587  f00 3596  foconst 3622  f1ococnv2 3647  f1ococnv1 3648  fvprc 3660  fv3 3672  tz6.12-2 3678  fvopabn 3725  elrnopabg 3739  exfo 3761  fopab2 3762  fsn 3773  fnressn 3776  tfrlem5 3854  tfrlem8 3857  tz7.48-2 3896  abianfp 3901  funoprabg 3949  curry1 4036  curry1f 4037  1stcof 4039  elrnoprabg 4062  oalimcl 4132  omlimcl 4147  brecop2 4245  ecopoprdm 4247  mapsn 4283  ixp0 4299  en2d 4335  dom2d 4339  fundmen 4363  unen 4368  pw2en 4380  sbthlem3 4383  sbthlem4 4384  sbthlem5 4385  sbthlem6 4386  sdomdomtr 4403  fodomr 4417  xpen 4420  mapenlem2 4422  mapdom2 4426  mapxpen 4427  xpmapenlem3 4430  xpmapenlem5 4432  mapunen 4434  pwen 4435  ssenen 4436  nneneq 4444  php 4445  isfinite1 4462  infn0 4464  ssfi 4467  unblem2 4470  isfinite2 4475  unfi 4480  unifi 4484  fiint 4486  abfii2 4488  pwfilem 4496  zfregcl 4519  elirrv 4522  inf3lem3 4539  inf3lem6 4542  infeq5 4545  noinfep 4564  zfregs 4571  r1val1 4582  rankr1 4598  rankuni 4622  rankval4 4626  rankc2 4630  rankelun 4631  rankelpr 4632  rankelop 4633  rankxplim 4636  rankxplim3 4638  rankxpsuc 4639  hta 4652  aceq3lem 4656  aceq5lem4 4662  aceq5 4664  ac6lem 4678  ac9s 4688  kmlem1 4689  kmlem4 4692  kmlem5 4693  kmlem7 4695  kmlem11 4699  zorn2lem4 4715  zorn2lem6 4717  zorn 4721  fodomb 4724  brdom3 4725  brdom5 4726  brdom4 4727  imadomg 4730  cardmin 4783  cardprc 4784  alephnbtwn 4791  cardaleph 4808  alephval3 4826  cflem 4828  cfval 4829  cfeq0 4837  cdavalt 4842  nd1 4861  nd2 4862  axpownd 4876  zfcndext 4888  zfcndrep 4889  distrpq 4990  prn0 5016  prnmax 5022  genpn0 5029  genpnnp 5031  prlem934 5062  ltaddpr 5063  prlem936 5078  reclem2pr 5080  suplem1pr 5084  suppsr 5145  supsrlem6 5153  ltresr 5181  supre 5183  negeu 5278  lttri4t 5438  ltnsym2t 5457  renfdisj 5463  xrltnsym2t 5475  xrrebndt 5492  receu 5621  rec11i 5684  eqneg 5711  nnind 5836  nn1suc 5838  nnleltp1t 5852  nominpos 5941  lble 5945  bndndx 5971  xrsupsslem 5974  xrinfmsslem 5975  xrsupss 5976  xrinfmss 5977  supxrre 5981  elnnz 6043  elnnz1 6053  uzwo3 6117  icounlem 6296  snunioolem 6298  uzwo 6338  uzwoOLD 6339  nnwof 6342  elfzp1 6393  fzneuzt 6401  expnnvalt 6455  discrlem3 6539  nn0opthlem2 6546  nn0opth 6547  sqrlem13 6566  sqr2irrlem3 6607  crulem 6617  crne0 6621  creui 6625  replimt 6643  abssubne0t 6771  cvg1 6809  cvg2 6810  cvg3 6811  faclbnd4lem4 6839  dffsum 6887  serzfsum 6893  fsump1s 6902  fsum1ps 6907  fsumshft 6920  fsumcmp 6929  bcxmas 6965  clm3 6968  climreu 6989  climrecl 6998  climge0 7000  climubi 7040  dfisum 7078  infcvglem1 7107  infcvglem3 7109  cvgratlem5 7140  fsum0diag4 7147  cncffvrn 7159  abscncflem 7160  mulc1cncf 7165  ivthlem3 7169  ivthlem5 7171  ivthlem6 7172  ivthlem7 7173  ivthlem4OLD 7179  ivthlem5OLD 7180  ivthlem6OLD 7181  ivthlem7OLD 7182  efseq0ex 7204  efclt 7205  efcvg 7207  efcvgfsum 7208  reeftlclt 7273  eflt 7298  efcnlem1 7310  efcn 7314  sinbndt 7358  cosbndt 7359  acdc5lem1 7384  acdcALT 7389  unbenlem 7398  infxpidmlem7 7452  infxpidmlem8 7453  infxpidmlem10 7455  infxpidmlem11 7456  infxpidmlem12 7457  iunctb 7468  basgen2t 7532  subbas 7537  fctop 7543  cctop 7545  clsval 7570  uncld 7574  ntrval2 7579  cmclsopn 7586  cmntrcld 7587  elcls 7596  neif 7604  0nnei 7615  islp2 7636  clslp 7637  qdensere 7639  idcn 7653  ismsg 7687  metreslem 7710  blf 7732  cncfmet 7792  lmuni 7834  lmsslem 7835  lmfexlem1 7839  metcnp4 7852  xplmi 7855  xpcn 7858  oprcn 7859  bopcnlem1 7863  bopcnlem4 7866  bcthlem4 7884  bcthlem7 7887  bcthlem9 7889  bcthlem14 7894  bcthlem28 7908  bcthlem29 7909  bcthlem30 7910  bcthlem31 7911  bcthlem33 7913  grpideu 7935  grprn 7938  isgrp2i 7959  grpinvf 7962  grpdivf 7968  resgrprn 7978  resgrprnOLD 7979  grplactf1o 7982  nvvop 8108  nvmf 8143  sqcn 8207  va1cnlem 8214  ipf 8235  ip1cnilem2 8243  ip1cnilem3 8244  nmlno0lem 8320  siilem1 8377  ipblnfi 8382  ubthlem3 8397  minveclem26 8436  pilem1 8503  pilem2 8504  sinperlem2 8519  sincosq2sgn 8535  sincosq4sgn 8537  efifolem2 8551  efif1lem5 8562  efif1lem7 8564  circcltOLD 8569  effoiOLD 8580  grothinf 8633  ghomfo 8658  ghomgsg 8662  ghomf1olem 8663  cayleylem2 8677  esnnei 8750  cnvhmpha 8763  hmphsyma 8766  hmphre 8768  hmeogrp 8776  fillsb 8785  fipfil2 8789  efilcp 8795  filint2 8796  fgsb2 8799  efilcp2 8800  cnfilca 8801  dtt2 8812  trdom 8829  cnvtr 8832  homib 8918  hgrablkne0 8955  bcseq 9135  chcmh 9264  norm1ex 9273  shorth 9298  occllem4 9306  projlem24 9339  pjthlem11 9358  pjtheu2 9379  pjoc1 9393  spanvalt 9428  hsupval2t 9429  shlej1 9477  shs00 9502  chj00 9539  chabs2t 9569  h1de2 9605  cmbr4 9675  spansnm0 9726  nonbool 9727  5oalem5 9734  pjssm 9757  pjvect 9772  pjocvect 9773  hoaddclt 9815  homulclt 9816  eigpos 9893  dmadjopt 9951  brafnt 10001  kbopt 10007  nmlnop0ALT 10049  lnopeq0 10061  nmcopexlem4 10083  nmcfnexlem4 10112  cnlnadjlem2 10130  cnlnadjlem3 10131  cnlnadjlem4 10132  cnlnadjlem5 10133  cnlnssadj 10142  nmopco 10156  cnvbravalt 10170  kbass2t 10176  pjss1co 10216  pjss2co 10217  pjorthco 10222  pjscj 10223  pjssdif2 10227  pjssdif1 10228  pjclem4 10251  pjc 10252  pj3s 10259  pj3cor1 10261  strlem3a 10303  strlem6 10307  hstrlem3a 10311  hstrlem6 10315  mdbr3 10348  mdbr4 10349  ssmd2 10361  mdslj1 10368  mdslj2 10369  mdsl2b 10372  cvmd 10373  mdslmd1lem1 10374  mdslmd1lem2 10375  hatomistic 10411  chrelat2 10414  atssmat 10427  atoml2 10432  irredlem1 10439  irredlem2 10440  mdsymlem1 10452  mdsymlem2 10453  mdsymlem5 10456  dmdbr5at 10469

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 147

Copyright terms: Public domain