Theorem sylibr 198

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

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

This theorem is referenced by:  3imtr4i 217  orrd 231  jca 286  imp3a 359  impbid 519  con4bid 527  con2bid 529  pm5.74rd 591  ibd 597  oibabs 657  pm5.18 663  pm5.75 754  ecase2d 756  3mix1 821  3mix2 822  3jca 825  ecase23d 929  19.8a 1065  19.29 1107  19.39 1118  19.24 1119  19.34 1129  hbim1 1139  equs4 1187  a4ime 1197  a4imed 1198  sb2 1214  sbequ1 1215  sbn 1268  a4sbe 1280  ax11eq 1402  ax11el 1403  a12study 1417  mo 1432  eu2 1435  exmo 1455  2euex 1481  2mo 1487  2eu6 1494  bm1.1 1504  eqrdv 1516  abbid 1619  abbi2dv 1621  abbi1dv 1622  necon3bi 1650  necon2ai 1654  alral 1738  ra4e 1741  rgen2a 1745  r19.21ai 1758  r19.29 1802  elisset 1863  cgsex2g 1878  cgsex4g 1879  cla42egv 1910  cla43egv 1912  rcla4e 1918  ceqex 1932  elab3g 1948  mo2icl 1969  reu6 1978  elrabsf 2011  ssrdv 2122  eqssd 2131  3sstr4g 2154  syl5ss 2157  abssdv 2173  ssrabdv 2178  ss2rabdv 2179  rabss2 2181  pssn2lp 2199  psstr 2202  ssun1 2245  uneqin 2308  reuss2 2327  ne0i 2338  vss 2360  disjne 2368  minel 2377  disjsn 2502  disjsn2 2503  difsn 2528  sspr 2540  elunii 2574  uniss 2588  uniss2 2596  unidif 2597  ssunieq 2598  intmin 2620  intab 2627  iunss1 2642  ssiun2 2661  iunss2 2663  iunxdif2 2666  3brtr4g 2720  trin 2764  axnul2 2782  class2seteq 2809  notzfaus 2815  pwuni 2837  opprc3 2873  opthwiener 2884  ssopab2 2900  sotric 2939  so 2943  frirr 2954  fr0 2956  epfrc 2961  wereu 2972  ordelord 2997  ordsseleq 3004  ordtri3or 3007  ordtri1 3008  orddisj 3013  suctr 3055  ordnbtwn 3062  reucl2 3111  mouniss 3113  reusni 3116  rabsnt 3117  reuhyp 3128  eldifpw 3133  elpwun 3134  elpwunsn 3135  iunpw 3137  dfwe2 3140  ordon 3141  ssorduni 3147  onint0 3153  suceloni 3170  ordsucss 3175  ordsucelsuc 3178  ordunisuc2 3198  ordzsl 3199  dflim3 3201  limuni3 3206  tfi 3207  omsson 3223  ordom 3228  omssnlim 3232  peano5 3241  xpsspw 3346  relop 3365  issetid 3370  cnvss 3381  opeldm 3405  dmcosseq 3452  relssres 3482  cotr 3528  dminss 3547  imainss 3548  xpnz 3551  cores 3602  relssdmrn 3617  relrelss 3618  funeu 3642  dffun8 3645  funco 3655  funun 3659  fununi 3668  funcnvuni 3669  funimaexg 3681  isarep2 3684  fnco 3701  fn0 3711  funimadisj 3712  zfrep6 3721  fnopabg 3722  fss 3742  fco 3743  funssxp 3745  fssres 3750  feu 3754  fcnvres 3755  fimacnvdisj 3756  fabexg 3760  f00 3764  fconst 3765  f1co 3774  fores 3789  foconst 3791  dff1o2 3801  dff1o3 3802  f1f1orn 3807  foimacnv 3814  f1oun 3815  fo00 3826  fv3 3844  tz6.12-1 3847  fvelrn 3926  dff2 3930  dff3 3931  dffo4 3934  exfo 3936  fopab2 3937  ffnfv 3942  fsn 3948  abrexex 3974  dff1o6 3991  f1oiso 4018  eloprabg 4067  fnoprabg 4072  ndmoprass 4109  ndmoprdistr 4110  fo1stres 4156  fo2ndres 4157  1stcof 4160  unielxp 4167  1stconst 4190  2ndconst 4191  curry1 4193  curry2 4196  iunon 4207  iinon 4208  onfununi 4209  onopriun 4211  tfrlem10 4221  tfr3 4227  tz7.44-3 4231  tz7.48lem 4256  tz7.48-1 4257  tz7.49 4260  tz7.49c 4261  abianfp 4263  oawordeulem 4324  oalimcl 4330  omlimcl 4345  oeordi 4350  oelim2 4358  oaabslem 4391  omsmo 4397  erdisj 4426  ecelqsi 4432  ecopoprtrn 4452  th3qlem1 4455  mapval2 4476  fpm 4479  map0b 4484  mapsn 4486  mapss 4487  ixpf 4497  ixpexg 4499  ixpssmap 4504  relsdom 4515  en2d 4541  dom2d 4545  ssdomg 4549  pw2en 4587  ac6sfilem3 4590  sbthlem2 4593  sbthlem3 4594  sbthlem7 4598  sbthlem8 4599  fodomr 4628  pwuninel 4631  2pwuninel 4632  pwne 4633  2pwne 4634  mapenlem2 4637  mapdom2lem 4640  mapxpen 4642  mapunen 4649  limenpsi 4652  php2 4661  php3 4662  ominf 4675  pssnn 4681  ssnnfi 4682  ssfi 4683  xpfi 4685  unblem1 4686  unblem2 4687  unfilem3 4696  unfi 4697  unfi2 4698  unifi2 4702  abfii2 4705  abfii3 4706  abfii4 4707  pwfilem 4713  pwfi 4714  supeu 4721  suppr 4733  supsnALT 4735  inf3lem3 4760  inf3lem6 4763  isfinite 4780  nnsdom 4781  infensuc 4784  trcl 4791  setind 4794  r1tr 4800  r1ord 4801  r1val1 4804  tz9.12lem1 4805  tz9.12lem3 4807  tz9.13 4809  rankon 4817  r1pw 4832  rankxplim3 4860  rankxpsuc 4861  scottex 4862  scott0 4863  aceq5 4886  aceq6a 4887  aceq6b 4888  ac6lem 4900  kmlem4 4914  kmlem6 4916  kmlem8 4918  kmlem13 4923  zorn2lem6 4939  zorn2lem7 4940  zorn 4943  fodom 4944  brdom3 4947  brdom5 4948  brdom4 4949  oncardval 4965  oncardon 4966  oncardid 4967  carden 4979  cardsn 4982  entric 4988  entri2 4989  cardsdomel 5002  ondomon 5006  ondomcard 5007  cardmin 5010  alephnbtwn 5018  alephval2 5052  alephval3 5053  cfub 5058  cflim 5059  cardcf 5061  cflecard 5062  cfsuc 5065  cfom 5066  nnacda 5090  addclpi 5174  mulclpi 5175  recmulpq 5224  prnmadd 5254  genpn0 5260  genpnnp 5262  genpcl 5265  1pr 5271  psslinpr 5289  prlem934 5293  ltexprlem1 5296  ltexprlem4 5299  ltexprlem5 5300  ltexprlem7 5302  reclem1pr 5310  reclem2pr 5311  reclem3pr 5312  mulgt0sr 5368  suppsr3 5378  axaddrcl 5426  axmulrcl 5428  axrnegex 5437  axcnre 5440  pre-axsup 5445  ltxrlt 5654  renepnf 5691  renemnf 5692  ssxr 5694  msqge0i 5768  recextlem2 5839  mulnzcnopr 5854  nn1suc 6084  nnleltp1 6100  nnsubi 6102  nnrp 6197  rpaddcl 6206  rpmulcl 6207  rpdivcl 6208  lbreu 6213  infmxrcl 6254  nnnegz 6306  elnnz 6313  elnnz1 6323  msqznn 6367  uzind 6376  uzwo5OLD 6382  uzwo3lem1 6388  uzwo3lem2 6389  zmin 6391  znq 6397  qaddcl 6408  qnegcl 6409  qmulcl 6410  qreccl 6412  flval3 6438  flge0nn0 6441  flge1nn 6442  zmodcl 6470  eliooord 6514  iccf 6528  eluz 6553  uztrn 6555  eluzaddi 6563  eluzsubi 6564  uzind4 6577  elfzuz 6616  elfznn 6624  elfznn0 6626  cardfz 6671  seq1f 6688  seq1f2 6689  ser1f 6693  shftf 6716  seqzval 6735  seqz1 6742  sqrlem5 6878  rpsqrcl 6916  sqr2irrlem1 6925  creur 6943  creui 6944  replim 6962  absrpcl 7057  nn0abscl 7082  abssubne0 7085  abs2dif 7105  seq1ublem 7114  cau3ii 7117  climeu 7303  climcmplem 7340  isumclimtfi 7399  infcvgaux2i 7424  mulc1cncf 7484  ivthlem7 7492  efseq1ex 7511  efaddlem2 7544  efaddlem27 7569  efne0 7574  reeftlcl 7585  ef01tllem1 7588  ef01tllem2 7589  ef01tllem2OLD 7590  absef01tllem 7592  eirrlem3 7596  reeff1 7618  efcnlem1 7627  efcn 7631  reeff1o 7634  acdc3lem 7697  acdc2lem2 7701  acdc5lem2 7704  acdclem 7706  infpn2 7721  infxpidmlem3 7766  infxpidmlem7 7770  infxpidmlem8 7771  infxpidmlem11 7774  infdif 7780  infpss 7786  infmap2lem2 7792  eltopsp 7816  tgval 7828  tgcl 7836  subbas2 7857  subtop 7858  sn0top 7859  distop 7861  cctop 7862  clscld 7893  elcls 7914  neips 7937  unnei 7945  lpval 7953  clslp 7958  idcn 7976  dnsconst 7998  bl2in 8053  opntop 8080  lpbl 8090  metcn 8100  tgioo 8126  lmcvgnns 8154  lmsslem 8163  lmfexlem1 8167  metelcls 8176  xplm 8186  xpcn 8187  iscms2 8205  lmcau 8207  cmsss 8208  bcthlem8 8217  bcthlem14 8223  bcthlem30 8239  isgrp 8254  grpfo 8256  grpideu 8266  grpinveu 8281  grpinvf 8297  issubg 8358  ablmul 8372  ringideu 8387  ringsn 8405  nvex 8477  isnv 8478  va1cnlem 8599  nmosetn0 8682  nmolb 8688  nmlno0lem 8708  isblo3i 8716  blocnilem 8719  blocni 8720  lnocni 8721  sspph 8771  ipblnfi 8772  ubthlem5 8791  ubthlem6 8792  ssphl 8881  htthlem11 8892  spwmo 8918  spweu 8919  cosh111lem1 8986  efif1lem5 9006  circgrp 9012  shftefif1olem 9013  axgroth3 9051  bcsiALT 9322  hlimreui 9386  hlimeui 9387  chsscmi 9388  hsn0elch 9396  hhsst 9412  ocsh 9432  occon 9436  occli 9457  projlem4 9465  projlem6 9467  projlem10 9471  projlem28 9489  projlem29 9490  pjthlem14 9508  pjtheui 9511  pjoc1i 9540  choc0 9566  choc1 9567  shintcli 9569  ococin 9573  hsupval2 9576  spancl 9580  hsupcl 9583  hsupss 9585  chsupsn 9588  spanss 9594  chlejb1i 9675  chabs2 9716  spanuni 9743  spansni 9756  spanunsni 9778  h1datomi 9780  cmbr3i 9819  cmbr4i 9820  lecmi 9821  osumlem5 9860  osumi 9864  osumcor2i 9868  nonbooli 9874  5oalem1 9877  5oalem2 9878  5oalem4 9880  5oalem5 9881  3oalem2 9886  pjss2i 9903  pjjsi 9923  pjmf1 9939  hmopex 10082  nmoplb 10111  unopf1o 10120  cnvunop 10122  unoplin 10124  counop 10125  nmfnlb 10128  adjvalval 10141  hmopadj2 10145  hmoplin 10146  bralnfn 10152  nmlnop0iALT 10199  lnopmi 10204  nmopun 10218  unopbd 10219  hmops 10224  hmopm 10225  hmopco 10227  nmcopexlem1 10230  nmcopexlem4 10233  nmcoplbi 10237  bdophmi 10241  lnopconi 10242  nmcfnexlem1 10259  nmcfnexlem4 10262  nmcfnlbi 10266  lnfnconi 10269  cnlnadjlem2 10280  cnlnadjlem3 10281  cnlnadjlem4 10282  cnlnadjlem5 10283  cnlnssadj 10292  adjbdln 10295  adjbdlnb 10296  adjlnop 10298  adjeq0 10303  branmfn 10317  branmfnOLD 10318  hmopidmchi 10359  hmopidmpji 10360  pjss2coi 10372  pjnormssi 10376  pjssdif2i 10382  pjinvari 10400  pjclem4 10408  pjci 10409  pjcmmul2i 10411  pj3si 10416  strlem1 10458  strlem3a 10460  hstrlem3a 10468  mdsl1i 10529  mdslmd3i 10540  csmdsymi 10542  mdexchi 10543  h1da 10557  shatomistici 10569  chpssati 10571  atomli 10591  irredi 10603  mdsymlem6 10617  sumdmdii 10624  cmmdi 10625  sumdmdlem2 10628  dmdbr5ati 10631  dmdbr6ati 10632  dmdbr7ati 10633  cdjreui 10641  cdj3i 10650  lediv2aALT 10656  ghomgrpilem2 10671  cayleylem1 10694  intn3an1d 10713  intn3an2d 10714  intn3an3d 10715  anddi2 10718  pm2.01bd 10722  ssoprab2g 10726  uninqs 10730  difeqri2 10732  elo 10733  ficli 10756  domrngref 10764  imgfldref2 10768  ref3w 10772  twpar2 10773  inttr 10787  restidsing 10805  imfstnrelc 10810  pospos 10882  tostos 10883  toplat 10884  opidon 10898  exidu1 10902  isppm 10917  seqzp2 10918  mndmgmid 10924  ismnd2 10928  expus 10938  rngmgmbs4 10945  unmnd 10951  ununr 10955  ring1cl 10966  cdrci 10994  bsi 10995  clint3 11002  topnem 11008  osneisi 11018  homeofval 11022  hmeogrp 11044  homcard 11045  eqindhome 11047  top2usne 11051  subtopsin2 11067  qusp 11068  oefil2 11079  neifil 11080  filintf 11081  fgsb 11082  efilcp 11083  fgsb2 11086  efilcp2 11087  cnfilca 11088  rcfpfillem2 11090  rcfpfillem4 11092  rcfpfillem6 11094  sfvlim 11100  dtopcl 11107  t2t1 11108  fintopcomp 11115  bwt2 11123  usinuniop 11128  dmse1 11146  iintlem1 11155  trnij 11160  dmrngcmp 11205  imonclem 11268  ismonc 11269  iepiclem 11278  isepic 11279  issubcat 11299  infemb 11313  eqeu 11394  trer 11409  finminlem 11418  fiss 11419  fiuni 11420  fictblem 11422  fictb 11423  ordiso 11426  ordtypelem4 11430  ordtypelem6 11432  ordtypelem7 11433  ordtype 11434  hartoglem 11435  hartog 11436  onsdom 11437  omsubsuc 11438  elomsubsd 11446  omsublim 11448  infenomsub 11450  opncldf1 11454  ntruni 11464  clsint2 11466  cnsubsp 11483  cnsubsp2 11484  compsublem 11487  compsub 11488  cptclsscpt 11489  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  dfcon2 11501  cnconn 11503  subtopmetlem 11505  reconnlem1 11507  reconnlem3 11509  reconnlem4 11510  reconnlem5 11511  2ndc1stc 11538  2ndcctbss 11539  isfne 11541  fneint 11547  isref 11549  fnessref 11564  refssfne 11565  lfinpfin 11574  locfincomp 11575  comppfsc 11578  neibastop1 11579  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  neibastop3 11585  topmtcl 11586  topmeet 11587  topjoin 11588  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  fnejoin2 11592  ist1-2 11603  fbasfip 11627  filfbas 11628  opnfbas 11629  fsubbas 11630  fgfil 11638  neifg 11644  supfil 11645  isufil2 11650  filssufillem 11655  filssufil 11656  ufileu 11658  fixufil 11661  ufinffr 11663  ufilen 11664  filcon 11665  ufcondr 11666  flimopn 11679  limfilcf 11683  flimcls 11684  cnpfillim 11686  elfilmap 11690  fmf 11693  fmbas 11694  filmapss 11696  rnelfmlem 11698  rnelfm 11699  fmfnfmlem4 11703  fmfnfm 11704  fmufil 11705  sfcls 11716  fclusss 11723  fcluscnplem 11729  fcluscomp 11733  tailmap 11759  tailuni 11761  tailfb 11762  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  filnet 11768  gafo 11773  ga0 11775  ssga 11777  gapm 11784  sylanbrc 11786  ralun 11789  respreima 11795  difxp 11798  oprabexd 11813  upixp 11823  ficard 11834  indexa 11845  fipreima 11848  fzfi 11864  sdclem1 11875  sdc 11877  seqpo 11878  incsequz2 11880  nnubfi 11881  nninfnub 11882  metsstop 11909  geomcau 11914  icoopnst 11940  iocopnst 11941  constcncf 11944  tlmval 11964  haustlmu 11967  txbas 11973  txuni 11975  txsubsp 11983  sstotbnd 11992  heiborlem11 12021  heiborlem13 12023  heiborlem17 12027  heiborlem18 12028  heiborlem23 12033  heiborlem27 12037  heiborlem29 12039  heiborlem30 12040  heiborlem32 12042  heiborlem35 12045  heiborlem36 12046  heiborlem38 12048  rrncms 12075  rrntotbndlem1 12076  rrntotbndlem2 12077  rrntotbnd 12078  reheibor 12081  iccbnd 12082  phtpycolem3 12095  phtpycolem4 12096  phtpycolem5 12097  phtpcer 12104  hgrablkcard 12200

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