Theorem sylibr 217

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

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

This theorem is referenced by:  3imtr4i 236  orrd 250  jca 310  imp3a 388  sylanbrc 527  con4bid 583  con2bid 585  pm5.74rd 648  ibd 654  oibabs 716  pm5.18OLD 723  pm5.75 821  pm5.75OLD 822  ecase2d 824  consensus 844  3mix1 1045  3mix2 1046  3jca 1050  19.8a 1376  19.29OLD 1422  19.39 1433  19.24 1434  19.34 1446  hbim1 1458  equs4 1510  a4ime 1521  sbn 1601  a4sbe 1613  ax11eq 1754  ax11el 1755  a12study 1769  mo 1787  eu2 1791  exmo 1812  2euexOLD 1845  2mo 1851  2eu6 1858  bm1.1 1870  eqrdv 1882  abbid 2007  abbi2dv 2009  abbi1dv 2010  necon3ai 2043  necon3biOLD 2046  necon2aiOLD 2052  alral 2153  ra4e 2156  rgen2a 2160  rgen2aOLD 2161  r19.21ai 2174  r19.27av 2224  r19.29OLD 2228  elissetOLD 2300  cgsex2g 2322  cgsex4g 2323  cla42egv 2366  cla43egv 2368  rcla4e 2375  ceqex 2391  elab3gOLDOLD 2411  mo2icl 2434  reu3 2444  elrabsf 2486  ssrdv 2622  3sstr4g 2658  syl5ss 2661  ss2abdv 2680  abssdv 2681  ss2rabdv 2687  rabss2OLD 2690  pssn2lpOLD 2710  ssun1 2767  uneqin 2845  uneqinOLD 2846  reuss2 2870  ne0i 2881  reximdva0 2886  vssOLD 2909  disjneOLD 2920  minel 2929  disjsnOLD 3090  disjsn2 3091  difsnOLD 3126  sspr 3144  elunii 3182  ssuni 3201  uniss2 3209  unidif 3210  ssunieq 3211  intminOLD 3238  intab 3247  ssiun2OLD 3296  iunss2 3298  iunxdif2 3301  3brtr4g 3369  trin 3422  truni 3425  trint 3426  axnulALT 3443  class2seteq 3472  notzfaus 3478  pwuni 3505  opprc3 3543  opthwiener 3554  sotric 3615  so 3620  frirr 3634  fr0 3636  epfrc 3642  epfrcOLD 3643  ordelord 3680  ordsseleqOLD 3688  ordtri3orOLD 3692  ordtri1 3693  ordtri1OLD 3694  orddisj 3701  suctr 3751  trsuc2 3754  mouniss 3816  reusni 3820  rabsnt 3821  eufromeq3 3830  eufromeq6 3833  rabxfrd 3842  reuhypd 3848  eldifpw 3854  elpwun 3855  elpwunsn 3856  iunpw 3858  dfwe2OLD 3862  ordon 3863  ssorduni 3870  ssorduniOLD 3871  onint0 3877  suceloni 3894  ordsucss 3899  ordsucelsuc 3902  ordsucelsucOLD 3903  ordunisuc2 3926  ordzsl 3927  limuni3 3936  tfi 3937  omssonOLD 3955  peano5 3975  xpsspw 4093  relop 4113  issetid 4121  issetidOLD 4122  cnvss 4134  opeldm 4160  dmcosseqOLD 4215  relssres 4248  cotrOLD 4303  dminss 4330  imainss 4331  xpnz 4335  coresOLD 4401  relrelss 4417  funeuOLD 4445  dffun8OLD 4449  funco 4457  funcoOLD 4458  funun 4462  funtp 4468  fnprg 4470  fntp 4471  fununi 4481  funcnvuni 4482  funimaexg 4495  isarep2 4499  fn0OLD 4533  funimadisj 4534  zfrep6 4545  fnopabg 4546  funssxp 4577  fssres 4582  feu 4588  fcnvres 4589  fimacnvdisj 4590  fabexg 4596  f00 4601  fconstOLD 4603  f1co 4612  fores 4627  foconst 4629  dff1o2OLD 4640  dff1o3OLD 4642  foimacnv 4657  f1oun 4658  fo00 4669  fv3 4690  tz6.12-1 4693  nfunsn 4706  dffv2 4734  fvelrn 4785  dff2 4789  dff3 4790  dffo4 4793  exfo 4795  fopab2 4796  ffnfv 4801  fsn 4807  fpr 4810  abrexex 4836  dff1o6 4853  eloprabg 4936  fnoprabg 4941  ndmoprass 4981  ndmoprdistr 4982  fo1stres 5036  fo2ndres 5037  unielxp 5047  1stconst 5070  2ndconst 5071  curry1 5075  iotanul 5098  iotacl 5103  iunon 5114  iinon 5115  onfununi 5116  onopriun 5118  tfrlem10 5128  tfr3 5134  tz7.44-3 5138  tz7.48lem 5164  tz7.48-1 5165  tz7.49 5168  tz7.49c 5169  abianfp 5171  oawordeulem 5236  oalimcl 5242  omlimcl 5257  oeordi 5262  oelim2 5270  oaabslem 5308  erdisj 5344  ecelqsi 5350  ecopoprtrn 5370  th3qlem1 5373  mapval2 5394  fpm 5397  map0b 5402  mapsn 5404  ixpf 5415  ixpexg 5417  ixpssmap 5422  relsdom 5433  ssdomg 5467  pw2en 5505  ac6sfilem3 5508  sbthlem2 5511  sbthlem3 5512  sbthlem7 5516  sbthlem8 5517  pwuninel 5550  2pwuninel 5551  pwne 5552  2pwne 5553  riota5 5580  mapenlem2 5584  mapdom2lem 5587  mapunen 5596  limenpsi 5599  php3 5609  ominf 5622  pssnn 5628  ssnnfi 5629  ssfi 5630  xpfi 5632  unblem1 5633  unblem2 5634  unfilem3 5643  unfi 5644  unfi2 5645  unifi2 5649  abfii2 5652  abfii3 5653  abfii4 5654  pwfilem 5660  pwfi 5661  supeu 5668  suppr 5680  supsnALT 5682  ordiso 5683  ordtypelem4 5687  ordtypelem7 5690  ordtype 5691  hartog 5693  inf3lem3 5721  inf3lem6 5724  isfinite 5741  nnsdom 5742  infensuc 5745  trcl 5752  en3lp 5758  setind 5759  r1tr 5765  r1ord 5766  r1val1 5769  tz9.12lem1 5770  tz9.12lem3 5772  tz9.13 5774  rankon 5782  r1pw 5797  rankxplim3 5825  rankxpsuc 5826  tratrb 5831  truniALT 5845  scottex 5846  scott0 5847  oncardval 5865  oncardon 5866  oncardid 5867  omsubsuc 5877  omsublim 5887  aceq5 5902  aceq6a 5903  aceq6b 5904  ac6lem 5916  kmlem4 5930  kmlem6 5932  kmlem8 5934  kmlem13 5939  zorn2lem6 5955  zorn2lem7 5956  zorn 5959  brdom3 5963  brdom5 5964  brdom4 5965  carden 5981  cardsn 5984  entric 5990  entri2 5991  ondomon 6008  alephnbtwn 6016  alephval2 6050  alephval3 6051  cflim 6057  cardcf 6059  cfsuc 6063  cfom 6064  nnacda 6088  recmulpq 6222  prnmadd 6252  genpn0 6258  genpnnp 6260  genpcl 6263  1pr 6269  psslinpr 6287  prlem934 6291  ltexprlem1 6294  ltexprlem4 6297  ltexprlem5 6298  ltexprlem7 6300  reclem1pr 6308  reclem2pr 6309  reclem3pr 6310  mulgt0sr 6366  suppsr3 6376  axaddrcl 6425  axmulrcl 6427  axrnegex 6436  axcnre 6439  pre-axsup 6444  ltxrlt 6669  renepnfOLD 6709  renemnfOLD 6711  ssxrOLD 6715  msqge0iOLD 6796  recextlem2 6875  mulnzcnopr 6891  nn1suc 7122  nnleltp1 7138  nnsubi 7140  lbreu 7254  infmxrcl 7295  nnnegz 7347  uzind 7417  uzwo3lem1 7429  uzwo3lem2 7430  zmin 7432  znq 7438  qaddcl 7449  qnegcl 7450  qmulcl 7451  qreccl 7453  iccf 7570  eluz 7595  uztrn 7597  elfzuz 7658  cardfz 7719  seq1f 7736  seq1f2 7737  ser1f 7741  seqzval 7783  seqz1 7790  sqrlem5 7927  sqr2irrlem1 7974  creur 7992  creui 7993  abssubne0 8134  seq1ublem 8163  cau3ii 8166  fz1fi 8229  climeu 8360  climcmplem 8397  isumclimtfi 8456  infcvgaux2i 8481  ivthlem7 8549  efseq1ex 8568  efaddlem27 8626  efne0 8631  reeftlcl 8642  ef01tllem1 8645  ef01tllem2 8646  ef01tllem2OLD 8647  absef01tllem 8649  eirrlem3 8653  efcnlem1 8684  reeff1o 8691  acdc3lem 8754  acdc2lem2 8758  acdc5lem2 8761  acdclem 8763  infpn2 8778  infxpidmlem3 8823  infxpidmlem7 8827  infxpidmlem8 8828  infxpidmlem11 8831  infdif 8837  infpss 8843  infmap2lem2 8849  eltopsp 8873  tgval 8886  subbas2 8915  subtop 8916  sn0top 8917  distop 8919  txbas 8933  txuni 8935  clscld 8959  elcls 8980  neips 9003  unnei 9011  clslp 9024  idcn 9042  bl2in 9120  lpbl 9157  metcn 9167  lmcvgnns 9221  lmsslem 9230  lmfexlem1 9234  metelcls 9243  iscms2 9272  bcthlem8 9284  bcthlem14 9290  bcthlem30 9306  isgrp 9321  grpfo 9323  grpideu 9333  grpinveu 9348  grpinvf 9364  ablmul 9439  gafo 9451  ga0 9453  ssga 9455  gapm 9462  ringideu 9470  ringsn 9490  nvex 9562  nmosetn0 9767  nmolb 9773  nmlno0lem 9793  blocnilem 9804  blocni 9805  lnocni 9806  ubthlem5 9876  ubthlem6 9877  spwmo 9999  spweu 10000  cosh111lem1 10068  efif1lem5 10088  circgrp 10094  shftefif1olem 10095  axgroth3 10138  twpar2 10149  dif1en 10172  fipreima 10175  ficard 10176  findcard 10178  cdrci 10182  fiuni 10219  filintf 10274  oefil2 10275  filfbas 10276  fsubbas 10281  fgfil 10290  sfvlim 10296  neifil 10302  filmapss 10309  fmf 10310  fmbas 10311  elfilmap 10312  flimopn 10321  cncomp 10331  usinuniop 10341  exidu1 10373  rngmgmbs4 10401  unmnd 10405  ring1cl 10415  bcsiALT 10679  hlimreui 10743  hlimeui 10744  chsscmi 10745  hsn0elch 10753  hhsst 10769  occon 10793  occli 10814  projlem4 10822  projlem6 10824  projlem28 10846  pjthlem14 10865  pjoc1i 10897  choc0 10923  choc1 10924  shintcli 10926  ococin 10930  hsupval2 10933  spancl 10937  hsupcl 10940  hsupss 10942  chsupsn 10945  spanss 10951  chlejb1i 11032  chabs2 11073  spanuni 11100  spansni 11113  spanunsni 11135  h1datomi 11137  cmbr3i 11176  cmbr4i 11177  lecmi 11178  osumlem5 11217  osumi 11221  osumcor2i 11225  nonbooli 11231  pjss2i 11260  pjjsi 11280  pjmf1 11296  hmopex 11439  nmoplb 11468  nmfnlb 11485  adjvalval 11498  nmlnop0iALT 11557  nmopun 11576  nmcopexlem1 11588  nmcopexlem4 11591  nmcoplbi 11595  lnopconi 11600  nmcfnexlem1 11617  nmcfnexlem4 11620  nmcfnlbi 11624  lnfnconi 11627  cnlnadjlem3 11639  cnlnadjlem4 11640  cnlnadjlem5 11641  cnlnssadj 11650  adjbdln 11653  adjbdlnb 11654  adjeq0 11661  branmfn 11675  branmfnOLD 11676  hmopidmchi 11723  pjss2coi 11736  pjnormssi 11740  pjssdif2i 11746  pjinvari 11764  pjci 11773  pjcmmul2i 11775  strlem1 11822  hstrlem3a 11832  mdsl1i 11893  mdslmd3i 11904  csmdsymi 11906  mdexchi 11907  chpssati 11935  atomli 11954  irredi 11966  mdsymlem6 11980  sumdmdii 11987  cmmdi 11988  sumdmdlem2 11991  dmdbr5ati 11994  dmdbr6ati 11995  dmdbr7ati 11996  cdjreui 12004  cdj3i 12013  bnj23 12397  bnj48OLD 12423  bnj112 12457  bnj145 12477  bnj168 12496  bnj215 12506  bnj214 12508  bnj219 12510  bnj512 12519  bnj534 12531  bnj542 12536  bnj592 12555  bnj596 12557  bnj851 12786  bnj863 12796  bnj869 12797  bnj875 12802  bnj876 12803  bnj877 12804  bnj905 12821  bnj927 12835  bnj1064 12900  bnj1072 12902  bnj1111 12924  bnj1142 12940  bnj1144 12941  bnj1161 12953  bnj1183 12965  bnj1184 12966  bnj1185 12967  bnj1197 12973  bnj1198 12974  bnj1199 12975  bnj1217 12990  bnj1218 12992  bnj1227 13000  bnj1298 13043  bnj1306 13049  bnj1310 13050  bnj1361 13086  bnj1363 13090  bnj1380 13097  bnj1379 13100  bnj1395 13109  bnj1396 13110  bnj1406 13116  bnj1427 13121  bnj1472 13149  bnj1477 13153  bnj1481 13158  bnj1483 13160  bnj1492 13161  bnj1494 13162  bnj1509 13169  bnj1542 13190  bnj56 13195  bnj97 13220  bnj102 13222  bnj103 13223  bnj109 13226  bnj127 13237  bnj129 13239  bnj149 13241  bnj218 13250  bnj513 13254  bnj522 13261  bnj535 13265  bnj545 13271  bnj546 13272  bnj548 13274  bnj549 13275  bnj571 13289  bnj578 13291  bnj605 13292  bnj594 13300  bnj580 13301  bnj607 13304  bnj600 13308  bnj849 13318  bnj917 13333  bnj934 13334  bnj944 13340  bnj950 13342  bnj964 13347  bnj966 13348  bnj967 13349  bnj969 13351  bnj910 13353  bnj978 13355  bnj986 13360  bnj996 13362  bnj1002 13367  bnj1031 13383  bnj1090 13410  bnj1097 13412  bnj1099 13413  bnj1100 13414  bnj1114 13419  bnj1121 13421  bnj1128 13428  bnj1137 13433  bnj1177 13445  bnj1228 13456  bnj1253 13470  bnj1287 13477  bnj1288 13478  bnj1367 13511  bnj1398 13515  bnj1404 13517  bnj1417 13530  bnj1421 13532  bnj1482 13551  bnj1498 13562  seq1resval 13617  seq1resval2 13618  lediv2aALT 13621  ghomgrpilem2 13629  cayleylem1 13641  suprzcl 13658  dvdslelem 13692  divalglem6 13701  divalglem8 13703  gcdcllem3 13720  gcdaddmlem 13734  algrf 13739  algrp1 13742  algcvgblem 13745  mulgcdlem2 13757  isprm2 13775  truniOLD 13792  trsuc2OLD 13793  trintOLD 13794  elres 13824  ressn0 13829  fundmpss 13836  dfon2lem4 13852  dfon2lem5 13853  dfon2lem7 13855  dfon2lem9 13857  dfon2 13858  dford4lem1 13859  predso 13895  trclss 13935  poxp 13949  soxp 13950  frxp 13951  wfrlem5 13961  wfrlem13 13969  noxpsgn 13990  nofv 13998  elno2 14005  axdenselem4 14022  axdenselem6 14024  axdenselem8 14026  axdense 14027  nocvxminlem 14028  axfelem4 14034  axfelem8 14038  axfelem9 14039  axfelem11 14041  axfelem12 14042  axfelem15 14045  axfelem16 14046  axfelem17 14047  brbigcup 14074  waj-ax 14238  trcrm 14286  anymptr 14289  evpexun 14322  ssoprab2g 14333  uninqs 14340  elo 14342  ficli 14353  domfldrefc 14361  ranfldrefc 14362  domrngref 14364  domintrefb 14367  imgfldref2 14368  ref4w 14370  srefwref 14373  inttr 14384  restidsing 14391  imfstnrelc 14396  dff1o6f 14416  fixpc 14418  isfinite1b 14434  trunitr 14438  uncum2 14441  inclrel 14444  inpreima2 14468  inpreima5 14469  fopab2g 14485  npincppr 14501  repfuntw 14502  repcpwti 14503  cbcpcp 14504  cbicplem 14508  unprj 14511  dstr 14516  domrancur1b 14548  domrancur1c 14550  tolat 14631  deref 14633  pospos 14635  rngsubpos 14636  tostos 14637  toplat 14638  isppm 14715  seqzp2 14716  expus 14726  curgrpact 14735  trooo 14758  ununr 14769  vecax3 14798  svli2 14826  bsi 14845  topnem 14858  cexint2 14862  osneisi 14875  hmeogrp 14892  homcard 14893  eqindhome 14895  top2usne 14898  stoig2b 14906  subtopsin2 14907  qusp 14908  usptoplem 14917  istopx 14918  prtoptop 14919  fgsb 14921  efilcp 14922  fgsb2 14925  efilcp2 14926  cnfilca 14927  rcfpfillem2 14929  rcfpfillem4 14931  rcfpfillem6 14933  elfilnemp 14935  dtopcl 14948  t2t1 14949  bwt2 14960  cntrsetlem 14999  dmse1 15001  iintlem1 15010  trnij 15015  dmrngcmp 15098  imonclem 15162  ismonc 15163  iepiclem 15172  isepic 15173  issubcat 15193  infemb 15207  tarax3d2 15225  tarcrpr 15237  tclinf 15241  intartar 15255  cartarlim 15282  fnctartar 15284  fnctartar2 15285  isline1 15294  trer 15361  finminlem 15367  fictblem 15370  fictb 15371  ordisoOLD 15374  ordtypelem4OLD 15378  ordtypelem7OLD 15381  ordtypeOLD 15382  hartogOLD 15384  omsubsucOLD 15386  omsublimOLD 15396  opncldf1 15402  ntruni 15412  clsint2 15414  cnsubsp2 15427  compsublem 15430  compsub 15431  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem2 15438  alexsublem3 15439  alexsublem4 15440  dfcon2 15442  reconnlem1 15446  reconnlem4 15449  reconnlem5 15450  2ndc1stc 15477  2ndcctbss 15478  isfne 15480  fneint 15486  isref 15488  lfinpfin 15513  locfincomp 15514  comppfsc 15517  neibastop1 15518  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  neibastop3 15524  topmtcl 15525  topmeet 15526  topjoin 15527  fnemeet1 15528  fnemeet2 15529  fnejoin1 15530  fnejoin2 15531  fbasfip 15556  opnfbas 15557  neifg 15559  supfil 15560  isufil2 15565  filssufillem 15570  filssufil 15571  ufileu 15573  fixufil 15576  ufinffr 15578  ufilen 15579  filcon 15580  ufcondr 15581  limfilcf 15587  cnpfillim 15589  rnelfmlem 15592  rnelfm 15593  fmfnfm 15598  sfcls 15604  fcluscnplem 15617  fcluscomp 15621  tailmap 15636  tailuni 15638  tailfb 15639  filnetlem3 15642  filnetlem4 15643  filnetlem5 15644  filnet 15645  ralunOLD 15657  cover2 15673  prfOLD 15680  respreima 15684  difxp 15690  oprabexd 15713  upixp 15729  eroprlem 15732  eropreu 15733  eroprf 15735  findcard2 15745  indexa 15753  fipreimaOLD 15756  infmrgelb 15766  wofi 15770  frfi 15771  pofun 15772  fzfi 15786  fzdisj 15793  sdclem1 15809  sdc 15811  fdc 15812  seqpo 15814  incsequz2 15816  nnubfi 15818  nninfnub 15819  geomcau 15849  icoopnst 15876  iocopnst 15877  constcncf 15882  tlmval 15903  haustlmu 15906  txsubsp 15912  txmet 15925  sstotbnd 15936  heiborlem11 15965  heiborlem13 15967  heiborlem17 15971  heiborlem18 15972  heiborlem23 15977  heiborlem27 15981  heiborlem29 15983  heiborlem30 15984  heiborlem32 15986  heiborlem35 15989  heiborlem36 15990  heiborlem38 15992  rrncms 16019  rrntotbndlem1 16020  rrntotbndlem2 16021  rrntotbnd 16022  reheibor 16025  iccbnd 16026  isgrpda 16033  phtpycolem3 16053  phtpycolem4 16054  phtpycolem5 16055  phtpcer 16062  pcoloopf 16079  pcohtpylem3 16082  pcopt 16084  pcorevlem 16086  pcorev 16087  isringd 16097  isdivrng2 16111  0idl 16173  divrngidl 16176  intidl 16177  unichnidl 16179  keridl 16180  ispridl2 16186  maxidln0 16193  igenval 16209  igenidl 16211  igenval2 16214  prnc 16215  isfldidl 16216  ispridlc 16218  prtlem90 16246  prtlem80 16247  eqrelrdv 16251  erprt 16276  prtlem18 16279  prter1 16282  hgrablkcard 16296  trelpss 16437  smoiso 16453  sspwtrALT2 16645  pwtr 16647  pwtrr 16649  snssiALT 16651  suctrALT2 16661  en3lpVD 16669  trintALT 16705  fnelstr 16717  strdif 16719  lubprop 16805  glbprop 16810  glbcon 17028  hl1atom 17040  grpideuNEW 17114  grpinveuNEW 17123  ringideuNEW 17146  pmap1 17247  pol1 17323  osumcllem10 17373  pexmidlem7 17384

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 164

Copyright terms: Public domain