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 515  con4bid 523  con2bid 525  pm5.74rd 587  ibd 593  oibabs 653  pm5.18 659  pm5.75 748  ecase2d 750  3mix1 814  3mix2 815  3jca 818  ecase23d 920  nicodraw 950  19.8a 1027  19.29 1069  19.39 1080  19.24 1081  19.34 1091  hbim1 1101  equs4 1148  a4ime 1158  a4imed 1159  sb2 1175  sbequ1 1176  sbn 1229  a4sbe 1241  ax11eq 1361  ax11el 1362  a12study 1376  mo 1391  eu2 1394  exmo 1414  2euex 1439  2mo 1445  2eu6 1452  bm1.1 1460  eqrdv 1471  abbid 1573  abbi2dv 1575  abbi1dv 1576  necon3bi 1604  necon2ai 1608  alral 1689  ra4e 1692  rgen2a 1696  r19.21ai 1709  r19.29 1753  elisset 1813  cgsex2g 1828  cgsex4g 1829  cla42egv 1860  cla43egv 1862  rcla4e 1868  ceqex 1882  elab3g 1898  mo2icl 1919  reu6 1928  elrabsf 1959  ssrdv 2066  eqssd 2075  3sstr4g 2098  syl5ss 2101  abssdv 2117  ssrabdv 2122  ss2rabdv 2123  rabss2 2125  pssn2lp 2143  psstr 2146  ssun1 2189  uneqin 2252  reuss2 2271  ne0i 2282  vss 2303  disjne 2311  minel 2320  disjsn 2437  disjsn2 2438  difsn 2460  sspr 2471  elunii 2503  uniss 2516  uniss2 2524  unidif 2525  ssunieq 2526  intmin 2548  intab 2555  iunss1 2569  ssiun2 2588  iunss2 2590  iunxdif2 2593  3brtr4g 2642  trin 2685  axnul2 2703  class2seteq 2730  notzfaus 2736  pwuni 2752  opprc3 2792  opthwiener 2802  ssopab2 2817  sotric 2855  so 2859  reucl2 2883  mouniss 2885  reusni 2888  rabsnt 2889  reuhyp 2900  eldifpw 2905  elpwun 2906  elpwunsn 2907  iunpw 2909  frirr 2919  fr0 2922  epfrc 2928  dfwe2 2930  wereu 2940  ordelord 2965  ordsseleq 2971  ordtri3or 2974  ordtri1 2975  orddisj 2980  ordon 2982  ssorduni 2988  onint0 3002  suceloni 3057  ordnbtwn 3058  ordsucss 3064  ordsucelsuc 3068  ordunisuc2 3110  ordzsl 3111  dflim3 3113  limuni3 3118  tfi 3121  omsson 3131  ordom 3136  omssnlim 3140  peano5 3148  xpsspw 3252  relop 3270  issetid 3275  cnvss 3286  opeldm 3309  dmcosseq 3357  relssres 3384  cotr 3428  dminss 3454  imainss 3455  xpnz 3458  cores 3491  relssdr 3505  funeu 3529  dffun7 3532  funco 3542  funun 3546  fununi 3555  funcnvuni 3556  funimaexg 3567  isarep2 3570  fnco 3587  fn0 3597  funimadisj 3598  zfrep6 3606  fnopabg 3607  fss 3626  fco 3627  funssxp 3629  fssres 3634  feu 3638  fcnvres 3639  fimacnvdisj 3640  fabexg 3644  f00 3648  fconst 3649  f1co 3658  fores 3672  foconst 3674  f1o2 3684  f1o3 3685  f1f1orn 3690  f1oun 3697  fo00 3706  fv3 3724  tz6.12-1 3727  fvelrn 3803  dff4 3807  dff2 3808  dffo4 3811  exfo 3813  fopab2 3814  ffnfv 3819  fsn 3825  abrexex 3851  f1ofv 3868  f1oiso 3895  iunon 3900  iinon 3901  tfrlem10 3911  tfr3 3917  tz7.44-3 3921  tz7.48lem 3946  tz7.48-1 3947  tz7.49 3950  tz7.49c 3951  abianfp 3953  eloprabg 3998  fnoprabg 4003  ndmoprass 4040  ndmoprdistr 4041  2ndconst 4087  curry1 4088  1stcof 4091  unielxp 4097  oawordeulem 4178  oalimcl 4184  omlimcl 4199  oeordi 4204  oelim2 4212  oaabslem 4241  omsmo 4247  erdisj 4276  ecelqsi 4282  ecopoprtrn 4301  th3qlem1 4304  mapval2 4325  fpm 4328  map0b 4333  mapsn 4335  mapss 4336  ixpf 4346  ixpexg 4348  ixpssmap 4353  relsdom 4362  en2d 4387  dom2d 4391  ssdomg 4395  pw2en 4432  sbthlem2 4434  sbthlem3 4435  sbthlem7 4439  sbthlem8 4440  fodomr 4469  pwuninel 4472  2pwuninel 4473  mapenlem2 4476  mapdom2lem 4479  mapxpen 4481  mapunen 4488  limenpsi 4491  php2 4500  php3 4501  ominf 4514  pssnn 4519  ssfi 4521  unblem1 4523  unblem2 4524  unfilem3 4532  unfi2 4535  unifi2 4539  abfii2 4542  abfii3 4543  abfii4 4544  pwfilem 4550  pwfi 4551  supeu 4558  suppr 4570  supsnALT 4572  inf3lem3 4595  inf3lem6 4598  isfinite 4614  nnsdom 4615  infensuc 4618  trcl 4625  setind 4628  r1tr 4634  r1ord 4635  r1val1 4638  tz9.12lem1 4639  tz9.12lem3 4641  tz9.13 4643  rankon 4651  r1pw 4666  rankxplim3 4694  rankxpsuc 4695  scottex 4696  scott0 4697  aceq5 4720  aceq6a 4721  aceq6b 4722  ac6lem 4734  kmlem4 4748  kmlem6 4750  kmlem8 4752  kmlem13 4757  zorn2lem6 4773  zorn2lem7 4774  zorn 4777  fodom 4778  brdom3 4781  brdom5 4782  brdom4 4783  oncardval 4799  oncardon 4800  oncardid 4801  carden 4811  cardsn 4814  entri 4819  entri2 4820  cardsdomel 4832  ondomon 4836  ondomcard 4837  cardmin 4840  alephnbtwn 4848  alephval2 4882  alephval3 4883  cfub 4888  cflim 4889  cardcf 4891  cflecard 4892  cfsuc 4895  cfom 4896  addclpi 5000  mulclpi 5001  recmulpq 5050  prnmadd 5080  genpn0 5086  genpnnp 5088  genpcl 5091  1pr 5097  psslinpr 5115  prlem934 5119  ltexprlem1 5122  ltexprlem4 5125  ltexprlem5 5126  ltexprlem7 5128  reclem1pr 5136  reclem2pr 5137  reclem3pr 5138  mulgt0sr 5194  suppsr3 5204  axaddrcl 5252  axmulrcl 5254  axrnegex 5263  axcnre 5266  pre-axsup 5271  ltxrltt 5480  renepnft 5518  renemnft 5519  ssxr 5521  msqge0 5596  recextlem2 5664  mulnzcnopr 5679  nn1suc 5895  nnleltp1t 5909  nnsub 5911  lbreu 6000  infmxrcl 6041  nnnegz 6093  elnnz 6100  elnnz1 6110  msqznn 6151  uzind 6161  uzwo5OLD 6167  uzwo3lem1 6172  uzwo3lem2 6173  zmin 6175  flval3t 6190  flge0nn0t 6193  flge1nnt 6194  znq 6204  qaddclt 6215  qnegclt 6216  qmulclt 6217  qrecclt 6219  rpaddclt 6235  rpmulclt 6236  rpdivclt 6237  seq1f 6268  seq1f2 6269  ser1ft 6273  shftf 6296  ioossicc 6338  iccf 6342  eluzt 6366  uztrn 6368  eluzaddi 6376  eluzsubi 6377  uzind4 6390  elfzuzt 6428  elfznnt 6434  elfznn0t 6436  seqzvalt 6480  seqz1 6487  sqrlem5 6615  rpsqrclt 6653  sqr2irrlem1 6662  creur 6681  creui 6682  replimt 6700  absrpclt 6798  nn0absclt 6824  abssubne0t 6828  abs2dift 6847  seq1ublem 6856  cau3i 6859  climeu 7045  climcmplem 7081  ser1f0 7114  isumclimtf 7139  infcvgaux2 7163  mulc1cncf 7222  ivthlem7 7230  ivthlem7OLD 7239  efseq1ex 7256  efaddlem2 7289  efaddlem27 7314  efne0t 7319  efsubt 7321  reeftlclt 7330  ef01tllem1 7333  ef01tllem2 7334  absef01tllem 7336  eirrlem3 7340  reeff1 7358  efcnlem1 7367  efcn 7371  reeff1o 7376  acdc3lem 7436  acdc2lem2 7439  acdc5lem2 7442  acdclem 7444  infpn2 7460  infxpidmlem3 7505  infxpidmlem7 7509  infxpidmlem8 7510  infxpidmlem11 7513  infdif 7519  infmap2lem2 7530  eltopsp 7554  tgvalt 7566  tgclt 7574  subbas2 7595  subtop 7596  sn0top 7597  distop 7599  fctop 7600  cctop 7602  clscld 7633  elcls 7654  neips 7677  unnei 7685  lpval 7693  clslp 7698  idcn 7716  dnsconst 7738  bl2in 7795  opntop 7822  lpbl 7832  metcn 7841  tgioo 7867  lmcvgnns 7895  lmsslem 7903  lmfexlem1 7907  metelcls 7916  xplm 7925  xpcn 7926  iscms2 7944  lmcau 7946  cmsss 7947  bcthlem8 7956  bcthlem14 7962  bcthlem30 7978  isgrp 7991  grpfo 7993  grpideu 8003  grpinveu 8014  grpinvf 8029  resgrprnOLD 8046  issubg 8068  ablmul 8083  ringsn 8115  nvex 8182  isnv 8183  va1cnlem 8292  nmosetn0 8373  nmolb 8379  nmlno0lem 8398  isblo3i 8405  blocnilem 8408  blocni 8409  lnocni 8410  sspph 8459  ipblnfi 8460  ubthlem5 8477  ubthlem6 8478  ssphl 8562  htthlem11 8573  spwmo 8598  spweu 8599  cosh111lem1 8648  efif1lem5 8668  circcltOLD 8675  circgrp 8679  shftefif1olem 8680  eff1i 8683  axgroth3 8718  bcsALT 8985  hlimreu 9049  hlimeu 9050  chsscm 9051  hsn0elch 9059  hhsst 9075  ocsh 9095  occont 9099  occl 9120  projlem4 9128  projlem6 9130  projlem10 9134  projlem28 9152  projlem29 9153  pjthlem14 9170  pjtheu 9173  pjoc1 9202  choc0 9228  choc1 9229  shintcl 9231  ococint 9235  hsupval2t 9238  spanclt 9242  hsupclt 9245  hsupss 9247  chsupsn 9250  spanss 9256  chlejb1 9337  chabs2t 9378  spanun 9405  spansn 9419  spanunsn 9442  h1datom 9444  cmbr3 9483  cmbr4 9484  lecm 9485  osumlem5 9522  osum 9526  osumcor2 9530  nonbool 9536  5oalem1 9539  5oalem2 9540  5oalem4 9542  5oalem5 9543  3oalem2 9548  pjss2 9565  pjjs 9585  pjmf1 9601  hmopex 9742  nmoplbt 9771  unopf1ot 9779  cnvunopt 9781  unoplint 9783  counopt 9784  nmfnlbt 9787  adjvalvalt 9800  hmopadj2t 9804  hmoplint 9805  bralnfnt 9811  nmlnop0ALT 9858  lnopm 9863  nmopunt 9877  unopbdt 9878  hmopst 9883  hmopmt 9884  hmopcot 9886  nmcopexlem1 9889  nmcopexlem4 9892  nmcoplb 9896  bdophm 9900  lnopcon 9901  nmcfnexlem1 9918  nmcfnexlem4 9921  nmcfnlb 9925  lnfncon 9928  cnlnadjlem2 9939  cnlnadjlem3 9940  cnlnadjlem4 9941  cnlnadjlem5 9942  cnlnssadj 9951  adjbdlnt 9954  adjbdlnb 9955  adjlnopt 9957  adjeq0 9962  branmfnt 9976  hmopidmch 10017  hmopidmpj 10018  pjss2co 10030  pjnormss 10034  pjssdif2 10040  pjinvar 10057  pjclem4 10065  pjc 10066  pjcmmul2 10068  pj3s 10073  strlem1 10115  strlem3a 10117  hstrlem3a 10125  mdsl1 10185  mdslmd3 10196  csmdsym 10198  mdexch 10199  h1dat 10213  shatomistic 10225  chpssat 10227  atoml 10246  irred 10258  mdsymlem6 10272  sumdmdi 10278  cmmd 10279  sumdmdlem2 10282  dmdbr5at 10284  dmdbr6at 10285  cdjreu 10293  cdj3 10302  lediv2itALT 10305  ghomgrpilem2 10320  cayleylem1 10343  intn3an1d 10364  intn3an2d 10365  intn3an3d 10366  faimpex 10375  uninqs 10378  difeqri2 10380  elo 10381  ficli 10404  cdrci 10417  bsi 10418  topnem 10430  homeofval 10439  hmeogrp 10461  homcard 10462  qusp 10466  oefil2 10477  neifil 10478  filintf 10479  fgsb 10480  efilcp 10481  fgsb2 10485  efilcp2 10486  cnfilca 10487  dtopcl 10495  t2t1 10496  dmse1 10503  iintlem1 10512  trnij 10517  imonclem 10619  ismonc 10620  hgrablkcard 10646

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