Theorem sylib 173

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 133	. 2 |- (ps -> ch)
4	1, 3	syl 12	1 |- (ph -> ch)

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  3imtr3 191  ord 202  exp3a 292  imdistand 342  bicomd 399  pm2.85 439  pm5.74d 444  mpbidi 447  negbid 463  pm5.32d 491  pm5.18 497  ecase2d 558  consensus 574  3mix3 602  ecased 643  19.23ad 748  nexd 780  sbf 870  hbs1f 874  sbequi 876  sbn1 880  sbea4 894  sbia4 895  sbba4 896  sbied 903  sb5f1 917  sb8 918  sb9i 920  eu2 1023  mooran1 1049  2eu1 1067  cleqcomd 1106  r19.21bi 1266  nrexdv 1271  elex 1356  ceqsalg 1362  cla4gf 1394  axrep 1473  zfrep2 1475  zfrep3 1476  3sstr3g 1540  syl6ss 1546  reuxfr2 1579  reuhyp 1581  un00 1728  npss0 1731  disjpss 1738  class2set 1747  ssnelpss 1751  pssnel 1752  sneqr 1856  preqr1 1872  preq12b 1874  exss 1881  opth 1898  opthwiener 1914  pwssun 1917  difex2 1951  euuni 1954  reucl 1957  reuuni3 1958  ssiun 2018  iununi 2037  iunpw 2040  3brtr3g 2087  sotric 2148  efrn2lp 2181  epne3 2182  dfwe2 2187  wecmpep 2193  wereu 2197  ordtri3or 2230  ordtri1 2231  ordtri3 2234  ordeleqon 2241  tfi 2244  sucexg 2302  suceloni 2314  ordnbtwn 2316  orddif 2326  orduniss 2327  ordtri2or 2328  ordsucun 2333  ordunisuc 2339  suc11 2341  onelin 2351  onelun 2352  onuninsuc 2356  limsuc 2361  limsssuc 2362  nlimsuc 2363  dflim3 2368  on0eqelt 2370  find 2396  finds2 2399  tfindsg2 2403  relss 2480  xpex 2488  dmxp 2552  resabs2 2593  iss 2599  imasn 2616  ndmima 2623  cnvexg 2669  funun 2700  funcnvuni 2706  funin 2708  funimacnv 2711  imadif 2714  fneu2 2729  fnssres 2734  fn0 2739  fnopabg 2745  fcoi1 2765  fcoi2 2766  feu 2767  fcnvres 2768  f00 2773  f1ococnv2 2817  f1ococnv1 2818  fvprc 2829  fv3 2839  tz6.12-2 2845  ndmfvrcl 2849  fnopabfv 2858  fniunfv 2860  fvopabn 2873  cleqfvf 2881  fopab2 2891  fsn 2895  fnressn 2897  tfrlem5 2953  tz7.48-1 2994  tz7.48-2 2995  abianfp 3000  oe0m1 3129  oalimcl 3162  nnmord 3189  brecop2 3243  ecopoprdm 3245  mapsn 3269  en2d 3303  dom2d 3307  fundmen 3333  unen 3338  pw2en 3348  sbthlem3 3351  sbthlem4 3352  sbthlem5 3353  sbthlem6 3354  sdomdomtr 3370  xpen 3383  mapenlem2 3385  mapdom2 3389  mapxpen 3390  xpmapenlem3 3393  xpmapenlem5 3395  mapunen 3397  pwen 3398  ssenen 3399  phplem1 3403  nneneq 3408  php 3409  isfinite1 3425  infn0 3427  pssnn 3428  ssfi 3430  unblem2 3432  isfinite2 3437  unfi 3441  fiint 3445  zfregcl 3446  eirrv 3449  inf3lem3 3466  inf3lem6 3469  inf3lem7 3470  inf5 3472  zfregs 3491  r1val1 3502  rankr1 3518  r1rankid 3537  ranklon 3540  aceq3lem 3555  aceq5lem4 3561  aceq5 3563  ac6lem 3575  kmlem1 3580  kmlem4 3583  kmlem5 3584  kmlem7 3586  kmlem10 3589  zornlem4 3606  zornlem6 3608  zorn2 3612  fodomb 3615  imadomg 3616  hta 3619  cardmin 3666  cardprc 3667  alephnbtwn 3674  alephgeom 3687  cardaleph 3690  cflem 3700  cfval 3701  cdavalt 3716  nd1 3732  nd2 3733  axpownd 3747  distrpq 3861  prn0 3887  prnmax 3893  genpn0 3900  genpnnp 3902  prlem934 3933  ltaddpr 3934  prlem936 3949  reclem2pr 3951  reclem3pr 3952  suplem1pr 3955  suppsr 4016  supsrlem6 4024  ltresr 4052  supre 4054  negeu 4124  receu 4215  rec11i 4261  eqneg 4378  nn1suc 4435  nnleltp1t 4448  nominpos 4509  crulem 4528  creui 4533  elnnz1 4581  nnwof 4609  uzwo3 4616  discrlem3 4715  nnesq 4720  nn0opthlem2 4723  nn0opth 4724  sqrlem13 4743  sqr2irrlem3 4779  replimt 4798  reim0 4809  infxpidmlem7 4939  infxpidmlem8 4940  infxpidmlem10 4942  infxpidmlem11 4943  infxpidmlem12 4944  bcseq 5073  chcmh 5148  shorth 5176  occllem4 5183  projlem24 5216  pjthlem11 5235  pjoc1 5268  pjoml 5271  shselt 5280  spanvalt 5300  hsupval2t 5301  shlej1 5349  shmods 5363  chj00 5408  chabs2t 5433  h1de2 5458  cmbr4 5510  5oalem1 5544  5oalem5 5548  pjssm 5572  pjss1co 5633  pjss2co 5634  pjorthco 5639  pjscj 5640  pjclem4 5653  pjc 5654  pj3s 5659  pj3cor1 5661  strlem3a 5693  strlem6 5697  mdbr3 5729  mdbr4 5730  ssmd2 5735  hatomistic 5755  chrelat2 5758  mdsymlem1 5776  mdsymlem2 5777  mdsymlem5 5780

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

This theorem depends on definitions:  df-bi 128

metamath.org