Theorem sylibr 200

Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition.

Hypotheses

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

Assertion

Ref	Expression
sylibr	|- (ph -> ch)

Proof of Theorem sylibr

Step	Hyp	Ref	Expression
1		sylibr.1	. 2 |- (ph -> ps)
2		sylibr.2	. . 3 |- (ch <-> ps)
3	2	biimpr 152	. 2 |- (ps -> ch)
4	1, 3	syl 10	1 |- (ph -> ch)

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

This theorem is referenced by:  3imtr4 219  orrd 233  jca 288  imp3a 361  impbid 518  con4bid 526  con2bid 528  pm5.74rd 590  ibd 596  oibabs 656  pm5.18 662  pm5.75 751  ecase2d 753  3mix1 817  3mix2 818  3jca 821  ecase23d 924  nicodraw 954  19.8a 1031  19.29 1073  19.39 1084  19.24 1085  19.34 1095  hbim1 1105  equs4 1152  a4ime 1162  a4imed 1163  sb2 1179  sbequ1 1180  sbn 1233  a4sbe 1245  ax11eq 1365  ax11el 1366  a12study 1380  mo 1395  eu2 1398  exmo 1418  2euex 1444  2mo 1450  2eu6 1457  bm1.1 1465  eqrdv 1476  abbid 1579  abbi2dv 1581  abbi1dv 1582  necon3bi 1610  necon2ai 1614  alral 1695  ra4e 1698  rgen2a 1702  r19.21ai 1715  r19.29 1759  elisset 1820  cgsex2g 1835  cgsex4g 1836  cla42egv 1867  cla43egv 1869  rcla4e 1875  ceqex 1889  elab3g 1905  mo2icl 1926  reu6 1935  elrabsf 1966  ssrdv 2073  eqssd 2082  3sstr4g 2105  syl5ss 2108  abssdv 2124  ssrabdv 2129  ss2rabdv 2130  rabss2 2132  pssn2lp 2150  psstr 2153  ssun1 2196  uneqin 2259  reuss2 2278  ne0i 2289  vss 2311  disjne 2319  minel 2328  disjsn 2445  disjsn2 2446  difsn 2468  sspr 2479  elunii 2512  uniss 2525  uniss2 2533  unidif 2534  ssunieq 2535  intmin 2557  intab 2564  iunss1 2578  ssiun2 2597  iunss2 2599  iunxdif2 2602  3brtr4g 2652  trin 2695  axnul2 2713  class2seteq 2740  notzfaus 2746  pwuni 2763  opprc3 2803  opthwiener 2813  ssopab2 2828  sotric 2866  so 2870  reucl2 2894  mouniss 2896  reusni 2899  rabsnt 2900  reuhyp 2911  eldifpw 2916  elpwun 2917  elpwunsn 2918  iunpw 2920  frirr 2930  fr0 2933  epfrc 2939  dfwe2 2941  wereu 2951  ordelord 2976  ordsseleq 2982  ordtri3or 2985  ordtri1 2986  orddisj 2991  ordon 2993  ssorduni 2999  onint0 3013  suceloni 3068  ordnbtwn 3069  ordsucss 3075  ordsucelsuc 3079  ordunisuc2 3121  ordzsl 3122  dflim3 3124  limuni3 3129  tfi 3132  omsson 3142  ordom 3147  omssnlim 3151  peano5 3159  xpsspw 3263  relop 3281  issetid 3286  cnvss 3297  opeldm 3320  dmcosseq 3371  relssres 3398  cotr 3442  dminss 3468  imainss 3469  xpnz 3472  cores 3505  relssdr 3519  funeu 3543  dffun7 3546  funco 3556  funun 3560  fununi 3569  funcnvuni 3570  funimaexg 3581  isarep2 3584  fnco 3601  fn0 3611  funimadisj 3612  zfrep6 3620  fnopabg 3621  fss 3641  fco 3642  funssxp 3644  fssres 3649  feu 3653  fcnvres 3654  fimacnvdisj 3655  fabexg 3659  f00 3663  fconst 3664  f1co 3673  fores 3687  foconst 3689  f1o2 3699  f1o3 3700  f1f1orn 3705  f1oun 3712  fo00 3721  fv3 3739  tz6.12-1 3742  fvelrn 3818  dff4 3822  dff2 3823  dffo4 3826  exfo 3828  fopab2 3829  ffnfv 3834  fsn 3840  abrexex 3866  f1ofv 3883  f1oiso 3910  iunon 3915  iinon 3916  tfrlem10 3926  tfr3 3932  tz7.44-3 3936  tz7.48lem 3961  tz7.48-1 3962  tz7.49 3965  tz7.49c 3966  abianfp 3968  eloprabg 4013  fnoprabg 4018  ndmoprass 4054  ndmoprdistr 4055  2ndconst 4103  curry1 4104  1stcof 4107  unielxp 4113  oawordeulem 4194  oalimcl 4200  omlimcl 4215  oeordi 4220  oelim2 4228  oaabslem 4257  omsmo 4263  erdisj 4292  ecelqsi 4298  ecopoprtrn 4317  th3qlem1 4320  mapval2 4341  fpm 4344  map0b 4349  mapsn 4351  mapss 4352  ixpf 4362  ixpexg 4364  ixpssmap 4369  relsdom 4380  en2d 4406  dom2d 4410  ssdomg 4414  pw2en 4452  sbthlem2 4454  sbthlem3 4455  sbthlem7 4459  sbthlem8 4460  fodomr 4489  pwuninel 4492  2pwuninel 4493  mapenlem2 4496  mapdom2lem 4499  mapxpen 4501  mapunen 4508  limenpsi 4511  php2 4520  php3 4521  php3OLD 4522  ominf 4536  ominfOLD 4537  pssnn 4544  ssnnfi 4545  ssfi 4547  ssfiOLD 4548  unblem1 4551  unblem2 4552  unfilem3 4562  unfi 4563  unfi2 4565  unfi2OLD 4566  unifi2OLD 4571  pwfilem 4577  pwfilemOLD 4578  pwfi 4579  pwfiOLD 4580  supeu 4587  suppr 4599  supsnALT 4601  inf3lem3 4624  inf3lem6 4627  isfinite 4643  isfiniteOLD 4644  nnsdom 4645  infensuc 4648  trcl 4655  setind 4658  r1tr 4664  r1ord 4665  r1val1 4668  tz9.12lem1 4669  tz9.12lem3 4671  tz9.13 4673  rankon 4681  r1pw 4696  rankxplim3 4724  rankxpsuc 4725  scottex 4726  scott0 4727  aceq5 4750  aceq6a 4751  aceq6b 4752  ac6lem 4764  kmlem4 4778  kmlem6 4780  kmlem8 4782  kmlem13 4787  zorn2lem6 4803  zorn2lem7 4804  zorn 4807  fodom 4808  brdom3 4811  brdom5 4812  brdom4 4813  oncardval 4829  oncardon 4830  oncardid 4831  carden 4841  cardsn 4844  entri 4849  entri2 4850  cardsdomel 4863  ondomon 4867  ondomcard 4868  cardmin 4871  alephnbtwn 4879  alephval2 4913  alephval3 4914  cfub 4920  cflim 4921  cardcf 4923  cflecard 4924  cfsuc 4927  cfom 4928  addclpi 5032  mulclpi 5033  recmulpq 5082  prnmadd 5112  genpn0 5118  genpnnp 5120  genpcl 5123  1pr 5129  psslinpr 5147  prlem934 5151  ltexprlem1 5154  ltexprlem4 5157  ltexprlem5 5158  ltexprlem7 5160  reclem1pr 5168  reclem2pr 5169  reclem3pr 5170  mulgt0sr 5226  suppsr3 5236  axaddrcl 5284  axmulrcl 5286  axrnegex 5295  axcnre 5298  pre-axsup 5303  ltxrltt 5512  renepnft 5549  renemnft 5550  ssxr 5552  msqge0 5626  recextlem2 5695  mulnzcnopr 5714  nn1suc 5941  nnleltp1t 5956  nnsub 5958  lbreu 6047  infmxrcl 6088  nnnegz 6140  elnnz 6147  elnnz1 6157  msqznn 6198  uzind 6207  uzwo5OLD 6213  uzwo3lem1 6218  uzwo3lem2 6219  zmin 6221  flval3t 6241  flge0nn0t 6244  flge1nnt 6245  znq 6259  qaddclt 6270  qnegclt 6271  qmulclt 6272  qrecclt 6274  rpaddclt 6291  rpmulclt 6292  rpdivclt 6293  seq1f 6324  seq1f2 6325  ser1ft 6329  shftf 6352  eliooordt 6389  iccf 6402  eluzt 6427  uztrn 6429  eluzaddi 6437  eluzsubi 6438  uzind4 6451  elfzuzt 6489  elfznnt 6495  elfznn0t 6497  seqzvalt 6541  seqz1 6548  sqrlem5 6678  rpsqrclt 6716  sqr2irrlem1 6725  creur 6743  creui 6744  replimt 6762  absrpclt 6855  nn0absclt 6879  abssubne0t 6882  abs2dift 6902  seq1ublem 6911  cau3i 6914  climeu 7100  climcmplem 7137  ser1f0 7170  isumclimtf 7195  infcvgaux2 7220  mulc1cncf 7279  ivthlem7 7287  efseq1ex 7306  efaddlem2 7339  efaddlem27 7364  efne0t 7369  efsubt 7371  reeftlclt 7380  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  absef01tllem 7387  eirrlem3 7391  reeff1 7410  efcnlem1 7419  efcn 7423  reeff1o 7426  acdc3lem 7487  acdc2lem2 7490  acdc5lem2 7493  acdclem 7495  infpn2 7510  infxpidmlem3 7555  infxpidmlem7 7559  infxpidmlem8 7560  infxpidmlem11 7563  infdif 7569  infpss 7575  infmap2lem2 7582  eltopsp 7605  tgvalt 7615  tgclt 7623  subtop 7643  sn0top 7644  distop 7646  fctopOLD 7647  cctop 7649  clscld 7680  elcls 7701  neips 7724  unnei 7732  lpval 7740  clslp 7745  idcn 7763  dnsconst 7785  bl2in 7840  opntop 7867  lpbl 7877  metcn 7886  tgioo 7912  lmcvgnns 7940  lmsslem 7949  lmfexlem1 7953  metelcls 7962  xplm 7972  xpcn 7973  iscms2 7991  lmcau 7993  cmsss 7994  bcthlem8 8003  bcthlem14 8009  bcthlem30 8025  isgrp 8038  grpfo 8040  grpideu 8050  grpinveu 8060  grpinvf 8075  issubg 8112  ablmul 8127  ringsn 8159  nvex 8226  isnv 8227  va1cnlem 8341  nmosetn0 8424  nmolb 8430  nmlno0lem 8449  isblo3i 8457  blocnilem 8460  blocni 8461  lnocni 8462  sspph 8511  ipblnfi 8512  ubthlem5 8529  ubthlem6 8530  ssphl 8615  htthlem11 8626  spwmo 8652  spweu 8653  cosh111lem1 8709  efif1lem5 8729  circgrp 8735  shftefif1olem 8736  eff1i 8739  axgroth3 8774  bcsALT 9041  hlimreu 9105  hlimeu 9106  chsscm 9107  hsn0elch 9115  hhsst 9131  ocsh 9151  occont 9155  occl 9176  projlem4 9184  projlem6 9186  projlem10 9190  projlem28 9208  projlem29 9209  pjthlem14 9227  pjtheu 9230  pjoc1 9259  choc0 9285  choc1 9286  shintcl 9288  ococint 9292  hsupval2t 9295  spanclt 9299  hsupclt 9302  hsupss 9304  chsupsn 9307  spanss 9313  chlejb1 9394  chabs2t 9435  spanun 9462  spansn 9475  spanunsn 9497  h1datom 9499  cmbr3 9538  cmbr4 9539  lecm 9540  osumlem5 9577  osum 9581  osumcor2 9585  nonbool 9591  5oalem1 9594  5oalem2 9595  5oalem4 9597  5oalem5 9598  3oalem2 9603  pjss2 9620  pjjs 9640  pjmf1 9656  hmopex 9797  nmoplbt 9826  unopf1ot 9835  cnvunopt 9837  unoplint 9839  counopt 9840  nmfnlbt 9843  adjvalvalt 9856  hmopadj2t 9860  hmoplint 9861  bralnfnt 9867  nmlnop0ALT 9915  lnopm 9920  nmopunt 9934  unopbdt 9935  hmopst 9940  hmopmt 9941  hmopcot 9943  nmcopexlem1 9946  nmcopexlem4 9949  nmcoplb 9953  bdophm 9957  lnopcon 9958  nmcfnexlem1 9975  nmcfnexlem4 9978  nmcfnlb 9982  lnfncon 9985  cnlnadjlem2 9996  cnlnadjlem3 9997  cnlnadjlem4 9998  cnlnadjlem5 9999  cnlnssadj 10008  adjbdlnt 10011  adjbdlnb 10012  adjlnopt 10014  adjeq0 10019  branmfnt 10033  hmopidmch 10074  hmopidmpj 10075  pjss2co 10087  pjnormss 10091  pjssdif2 10097  pjinvar 10114  pjclem4 10122  pjc 10123  pjcmmul2 10125  pj3s 10130  strlem1 10172  strlem3a 10174  hstrlem3a 10182  mdsl1 10243  mdslmd3 10254  csmdsym 10256  mdexch 10257  h1dat 10271  shatomistic 10283  chpssat 10285  atoml 10304  irred 10316  mdsymlem6 10330  sumdmdi 10337  cmmd 10338  sumdmdlem2 10341  dmdbr5at 10344  dmdbr6at 10345  dmdbr7at 10346  cdjreu 10354  cdj3 10363  lediv2itALT 10366  ghomgrpilem2 10381  cayleylem1 10404  intn3an1d 10423  intn3an2d 10424  intn3an3d 10425  faimpex 10433  uninqs 10436  difeqri2 10438  elo 10439  ficli 10462  cdrci 10480  bsi 10481  topnem 10493  homeofval 10502  hmeogrp 10524  homcard 10525  eqindhome 10527  top2usne 10535  qusp 10541  oefil2 10552  neifil 10553  filintf 10554  fgsb 10555  efilcp 10556  fgsb2 10560  efilcp2 10561  cnfilca 10562  rcfpfillem2 10564  rcfpfillem4 10566  rcfpfillem6 10568  sfvlim 10576  dtopcl 10586  t2t1 10587  dmse1 10594  iintlem1 10603  trnij 10608  imonclem 10712  ismonc 10713  hgrablkcard 10745

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