Theorem sylibr 134

Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by NM, 5-Aug-1993.)

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

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylbbr  136  pm5.74rd  183  bitri  184  3imtr4i  201  sylanbrc  417  oibabs  715  dcim  842  dcstab  845  stdcndc  846  stdcndcOLD  847  dcand  934  dcor  937  3mix1  1168  3mix2  1169  3jca  1179  syl3anbrc  1183  syl21anbrc  1184  inegd  1391  pclem6  1393  xoranor  1396  dcfrompeirce  1468  nfxfrd  1497  nfd  1545  hban  1569  nfan1  1586  nford  1589  nfand  1590  hbim1  1592  nfal  1598  alexim  1667  nnal  1671  ax6blem  1672  nf4r  1693  19.34  1706  nfexd  1783  sbcof2  1832  nfsb2or  1859  sbidm  1873  nfdv  1899  nfd2  2049  nfeudv  2068  mon  2082  eumo  2085  mo23  2094  eu2  2097  eu3h  2098  exmodc  2103  exmonim  2104  mo2r  2105  mo3h  2106  bm1.1  2189  eqrdv  2202  3eltr4g  2290  abbi2dv  2323  abbi1dv  2324  nfcd  2342  nfcxfrd  2345  dcned  2381  neqned  2382  3netr4g  2410  necon3bi  2425  necon2ai  2429  nnral  2495  alral  2550  rspe  2554  rsp2e  2556  rgen2a  2559  ralrimi  2576  r19.27v  2632  r19.28v  2633  r19.27av  2640  r19.32r  2651  nfreudxy  2679  mormo  2721  nrexrmo  2726  cgsex2g  2807  cgsex4g  2808  spc2egv  2862  spc2gv  2863  spc3egv  2864  spc3gv  2865  rspce  2871  ceqex  2899  elrab3t  2927  elrabd  2930  mosubt  2949  mo2icl  2951  reu3  2962  reu6i  2963  2rmorex  2978  sbc5  3021  rspesbca  3082  rmo2ilem  3087  sbnfc2  3153  ssrd  3197  ssrdv  3198  3sstr4g  3235  eqsstrid  3238  ss2abdv  3265  abssdv  3266  rabssdv  3272  ss2rabdv  3273  ssun1  3335  unssad  3349  unssbd  3350  ssddif  3406  uneqin  3423  indifdir  3428  undif3ss  3433  reuss2  3452  n0rf  3472  reximdva0m  3475  rabxmdc  3491  ssindif0im  3519  minel  3521  ralidm  3560  ralm  3563  dcun  3569  ifmdc  3611  disjsn2  3695  absneu  3704  rabsneu  3705  opprc  3839  elunii  3854  dfnfc2  3867  uniss2  3880  unidif  3881  ssunieq  3882  intab  3913  iunss2  3971  iunssd  3972  iunxdif2  3975  invdisj  4037  disjiun  4038  3brtr4g  4077  trin  4151  triun  4154  truni  4155  trint  4156  iinexgm  4197  class2seteq  4206  pwuni  4235  exmid1dc  4243  exmidn0m  4244  exmidsssn  4245  exmid0el  4247  exmidel  4248  exmidundif  4249  exmidundifim  4250  exmid1stab  4251  mss  4269  copsex2t  4288  euotd  4298  pwunim  4332  ispod  4350  sotricim  4369  exse  4382  frind  4398  trssord  4426  suctr  4467  pwnex  4495  eusvnf  4499  eusvnfb  4500  eusv2nf  4502  rexxfrd  4509  ralxfr2d  4510  rexxfr2d  4511  rabxfrd  4515  reuhypd  4517  eldifpw  4523  iunpw  4526  ssorduni  4534  onsucb  4550  onsucelsucr  4555  sucunielr  4557  ontriexmidim  4569  ordtri2or2exmidlem  4573  onsucelsucexmid  4577  reg2exmidlema  4581  setindel  4585  elirr  4588  orddisj  4593  en2lp  4601  suc11g  4604  ordsuc  4610  nlimsucg  4613  ordtri2or2exmid  4618  ontri2orexmidim  4619  zfregfr  4621  wessep  4625  tfi  4629  peano5  4645  limom  4661  peano2b  4662  nndceq0  4665  nnpredcl  4670  0nelrel  4720  eqrelrdv  4770  xpsspw  4786  relint  4798  relop  4827  eqbrrdva  4847  opeldm  4880  elres  4994  relssres  4996  elrelimasn  5047  exse2  5055  issref  5064  trin2  5073  dminss  5096  imainss  5097  rnxpid  5116  dmsn0el  5151  dmmptg  5179  relrelss  5208  cnviinm  5223  iotanul  5246  sniota  5261  dffun5r  5282  funmo  5285  funco  5310  funun  5314  fununmo  5315  fununfun  5316  funprg  5323  funtpg  5324  funtp  5326  fntpg  5329  fununi  5341  funcnvuni  5342  imadiflem  5352  imainlem  5354  funimaexglem  5356  isarep2  5360  fnunsn  5382  2elresin  5386  fnimadisj  5395  dmmptd  5405  fco  5440  funssxp  5444  fssres  5450  feu  5457  fimacnvdisj  5459  fabexg  5462  f00  5466  f0rn0  5469  f1co  5492  fores  5507  foco  5508  f1ores  5536  foimacnv  5539  f1oun  5541  fun11iun  5542  f1oco  5544  fo00  5557  brprcneu  5568  fv3  5598  relelfvdm  5607  nfvres  5609  nfunsn  5610  funfvbrb  5692  respreima  5707  dff2  5723  dff3im  5724  dffo4  5727  fvmptelcdm  5732  ffvresb  5742  f1oresrab  5744  fmptco  5745  fsn  5751  fpr  5765  ftpg  5767  fsnunf  5783  fsnunfv  5784  elabrex  5825  dff1o6  5844  foeqcnvco  5858  fliftel1  5862  isores1  5882  isoini2  5887  riotasbc  5914  acexmidlemph  5936  acexmidlemcase  5938  oprabidlem  5974  brabvv  5990  eloprabga  6031  fnoprabg  6045  caovimo  6139  oprabexd  6211  uchoice  6222  fo1stresm  6246  fo2ndresm  6247  unielxp  6259  1st2ndbr  6269  fmpoco  6301  1stconst  6306  2ndconst  6307  poxp  6317  spc2ed  6318  disjxp1  6321  reldmtpos  6338  tposfun  6345  dftpos4  6348  smores  6377  smores2  6379  tfrlem1  6393  tfr0dm  6407  tfrlemibxssdm  6412  tfrlemibex  6414  tfrlemiubacc  6415  tfrlemi14d  6418  tfrexlem  6419  tfri1d  6420  tfr1onlembxssdm  6428  tfr1onlembex  6430  tfr1onlemubacc  6431  tfr1onlemres  6434  tfrcllemsucfn  6438  tfrcllembxssdm  6441  tfrcllembex  6443  tfrcllemubacc  6444  tfrcllemres  6447  tfri3  6452  rdgon  6471  frecabcl  6484  frecfcllem  6489  frecrdg  6493  2oconcl  6524  nnsucelsuc  6576  nntri3or  6578  nndceq  6584  nndcel  6585  dcdifsnid  6589  ecexr  6624  brdifun  6646  ecelqsdm  6691  iinerm  6693  eroveu  6712  erovlem  6713  ecopovtrn  6718  ecopovtrng  6721  th3qlem1  6723  pmsspw  6769  map0b  6773  mapsn  6776  mapsncnv  6781  ixpf  6806  uniixp  6807  ixpexgg  6808  resixp  6819  f1oen3g  6844  ssdomg  6869  domtr  6876  snfig  6905  enpr2d  6910  xpf1o  6940  xpmapenlem  6945  php5dom  6959  fidceq  6965  nnfi  6968  fiunsnnn  6977  findcard  6984  findcard2  6985  findcard2s  6986  ac6sfi  6994  tridc  6995  fimax2gtri  6997  finexdc  6998  exmidpw  7004  exmidpweq  7005  exmidpw2en  7008  nnwetri  7012  unsnfi  7015  unsnfidcex  7016  unsnfidcel  7017  undifdcss  7019  tpfidisj  7025  tpfidceq  7026  iunfidisj  7047  snexxph  7051  fidcenumlemrks  7054  sbthlem2  7059  sbthlemi3  7060  sbthlem7  7064  sbthlemi8  7065  fival  7071  dcfi  7082  supmoti  7094  djuss  7171  updjudhf  7180  updjud  7183  casefun  7186  caseinj  7190  omp1eomlem  7195  djufun  7205  djuinj  7207  ctssdccl  7212  ctfoex  7219  nnnninf  7227  nnnninfeq2  7230  nninfisollem0  7231  nninfisollemne  7232  nninfisollemeq  7233  nninfisol  7234  finomni  7241  exmidomniim  7242  exmidomni  7243  fodjuomnilemdc  7245  omniwomnimkv  7268  nninfdcinf  7272  nninfwlporlem  7274  nninfwlpoimlemg  7276  nninfwlpoim  7280  nninfinfwlpo  7281  exmidonfinlem  7300  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  finacn  7315  exmidaclem  7319  dju1en  7324  exmidontriimlem1  7332  exmidontriimlem3  7334  pw1on  7337  3nsssucpw1  7347  2omotaplemap  7368  2omotap  7370  exmidmotap  7372  cc4f  7380  cc4n  7382  acnccim  7383  dmaddpqlem  7489  nqpi  7490  dmaddpq  7491  dmmulpq  7492  ltdcnq  7509  subhalfnqq  7526  enq0sym  7544  enq0ref  7545  enq0tr  7546  nqnq0pi  7550  nq0nn  7554  addnq0mo  7559  mulnq0mo  7560  nqpnq0nq  7565  nqnq0a  7566  nqnq0m  7567  npsspw  7583  elnp1st2nd  7588  prnmaxl  7600  prnminu  7601  prarloc  7615  genprndl  7633  genprndu  7634  nqprm  7654  nqprl  7663  nqpru  7664  addnqprlemrl  7669  addnqprlemru  7670  prmuloc  7678  mulnqprlemrl  7685  mulnqprlemru  7686  ltsopr  7708  ltexprlemm  7712  ltexprlemopl  7713  ltexprlemopu  7715  lteupri  7729  recexprlemopl  7737  recexprlemopu  7739  recexprlemdisj  7742  archpr  7755  cauappcvgprlemdisj  7763  cauappcvgprlemladdrl  7769  cauappcvgprlem2  7772  caucvgprlemnbj  7779  caucvgprlemdisj  7786  caucvgprlemladdfu  7789  caucvgprlem2  7792  caucvgprprlemnbj  7805  caucvgprprlemdisj  7814  suplocexprlemml  7828  suplocexprlemrl  7829  suplocexprlemmu  7830  suplocexprlemloc  7833  addsrmo  7855  mulsrmo  7856  recexgt0sr  7885  prsrpos  7897  caucvgsrlemasr  7902  suplocsrlemb  7918  suplocsrlempr  7919  suplocsr  7921  elrealeu  7941  pitonn  7960  pitoregt0  7961  pitore  7962  recnnre  7963  axaddcl  7976  axaddrcl  7977  axmulcl  7978  axmulrcl  7979  axrnegex  7991  axcnre  7993  axpre-lttrn  7996  rereceu  8001  axarch  8003  axpre-suploclemres  8013  axpre-suploc  8014  ltxrlt  8137  apirr  8677  divmulasscomap  8768  rerecclap  8802  lbreu  9017  arch  9291  0mnnnnn0  9326  nnm1nn0  9335  elnnnn0c  9339  elnnz1  9394  ztri3or0  9413  nzadd  9424  nn0n0n1ge2  9442  zdceq  9447  zdcle  9448  zdclt  9449  uzind  9483  eluzge3nn  9692  supinfneg  9715  infsupneg  9716  eluz2b2  9723  elnn1uz2  9727  elnn0dc  9731  elnndc  9732  nn01to3  9737  znq  9744  qaddcl  9755  qmulcl  9757  qreccl  9762  irradd  9766  irrmul  9767  elpq  9769  cnref1o  9771  xnn0dcle  9923  xrpnfdc  9963  xrmnfdc  9964  xaddcom  9982  xnegdi  9989  xpncan  9992  xleadd1a  9994  iooidg  10030  elioo4g  10055  elfzd  10137  fzdcel  10161  fznlem  10162  fzpreddisj  10192  fz0to4untppr  10245  elfz0ubfz0  10246  elfz0fzfz0  10247  fz0fzelfz0  10248  fz0fzdiffz0  10251  elfzmlbp  10253  difelfzle  10255  4fvwrd4  10261  fzosplit  10299  elfzo0  10304  fzo1fzo0n0  10305  elfzonn0  10308  fzofzim  10310  elfzo1  10312  elfzom1elp1fzo  10329  fzossfzop1  10339  ssfzo12bi  10352  exfzdc  10367  zsupcllemstep  10370  infssuzex  10374  qdceq  10385  qdclt  10386  exbtwnzlemstep  10388  exbtwnzlemex  10390  exbtwnz  10391  rebtwn2zlemstep  10393  rebtwn2z  10395  qbtwnxr  10398  modfzo0difsn  10538  frec2uzrand  10548  frec2uzf1od  10549  frecuzrdgrcl  10553  frecuzrdgtcl  10555  frecuzrdgrclt  10558  frecuzrdgfunlem  10562  frecfzennn  10569  nninfinf  10586  seq3f1olemp  10658  seq3f1oleml  10659  seqf1oglem1  10662  ser0f  10677  expcl2lemap  10694  hashunsng  10950  iswrdinn0  10997  snopiswrd  11002  wrdlndm  11009  iswrdsymb  11010  wrdsymb1  11028  ccatfv0  11057  ccatval21sw  11059  lswccatn0lsw  11065  eqs1  11080  ccat1st1st  11091  lswccats1fst  11094  shftfvalg  11100  shftfval  11103  caucvgre  11263  rexanuz  11270  recvguniq  11277  rennim  11284  resqrexlemf  11289  rsqrmo  11309  fimaxre2  11509  climeu  11578  sumdc  11640  summodc  11665  zsumdc  11666  isum  11667  fisumss  11674  isumss2  11675  fsumsplit  11689  sumsnf  11691  fsumsplitsn  11692  sumtp  11696  sumsplitdc  11714  fsum2dlemstep  11716  fisum0diag2  11729  fsumconst  11736  modfsummodlemstep  11739  fsum00  11744  fsumabs  11747  fsumiun  11759  isumlessdc  11778  expcnv  11786  prodmodc  11860  zproddc  11861  iprodap  11862  iprodap0  11864  fprodssdc  11872  prodsnf  11874  fprodsplitdc  11878  fprodsplit  11879  fprodm1  11880  fprod1p  11881  fprodunsn  11886  fprod2dlemstep  11904  fprodsplitsn  11915  ef0lem  11942  modmulconst  12105  dvdsdivcl  12132  dvdsssfz1  12134  dvdsfac  12142  zeoxor  12151  nn0ehalf  12185  nn0oddm1d2  12191  nnoddm1d2  12192  divalglemeunn  12203  divalglemeuneg  12205  bitsfzolem  12236  bitsinv1  12244  gcdsupex  12249  gcdsupcl  12250  bezoutlemnewy  12288  bezoutlemmain  12290  bezoutlemeu  12299  dfgcd2  12306  nnwosdc  12331  nninfct  12333  algrf  12338  algcvgblem  12342  lcmgcdlem  12370  lcmdvds  12372  coprmgcdb  12381  mulgcddvds  12387  qredeu  12390  cncongr1  12396  cncongr2  12397  isprm2lem  12409  dvdsnprmd  12418  prmdc  12423  oddprmge3  12428  pw2dvdseu  12461  phibndlem  12509  dfphi2  12513  hashdvds  12514  phiprmpw  12515  eulerthlemh  12524  hashgcdeq  12533  phisum  12534  odzdvds  12539  reumodprminv  12547  nnnn0modprm0  12549  prm23ge5  12558  pclemdc  12582  pcdvdsb  12614  difsqpwdvds  12632  oddprmdvds  12648  1arith  12661  4sqlem3  12684  4sqlemafi  12689  4sqlemffi  12690  4sqleminfi  12691  4sqexercise1  12692  4sqlem11  12695  4sqlem19  12703  ennnfonelemdc  12741  ennnfonelemh  12746  ennnfonelemhf1o  12755  ennnfonelemf1  12760  ennnfonelemrn  12761  ennnfonelemdm  12762  exmidunben  12768  ctinfomlemom  12769  ctinfom  12770  ctiunctlemudc  12779  ctiunctlemf  12780  ctiunctal  12783  nninfdclemcl  12790  nninfdclemf  12791  nninfdclemp1  12792  isstructim  12817  setsresg  12841  strleund  12906  1strbas  12920  2strbasg  12923  2stropg  12924  restsspw  13052  tgval  13065  ptex  13067  imasaddfnlemg  13117  fnpr2o  13142  fnpr2ob  13143  mgmidsssn0  13187  fngsum  13191  igsumvalx  13192  isnsgrp  13209  sgrpidmndm  13223  mndinvmod  13248  mnd1  13258  mhmeql  13295  grpinveu  13341  prdsinvlem  13411  mulgval  13429  subgintm  13505  trivsubgsnd  13508  eqgfval  13529  ecqusaddd  13545  ecqusaddcl  13546  ghmeql  13574  iscmnd  13605  imasabl  13643  gsumfzmhm2  13651  rnglz  13678  srgfcl  13706  reldvdsrsrg  13825  rhmopp  13909  subrgdvds  13968  lssuni  14096  lssintclm  14117  lspf  14122  qusmulrng  14265  mulgrhm2  14343  znf1o  14384  psrbagfi  14406  psr1clfi  14421  mplsubgfilemcl  14432  istopon  14456  toponcom  14470  topgele  14472  topontopn  14480  tsettps  14481  eltg2b  14497  unitg  14505  tgss2  14522  bastop2  14527  distop  14528  epttop  14533  cldss2  14549  neisspw  14591  neipsm  14597  neiuni  14604  tgcn  14651  tgcnp  14652  cnntr  14668  lmff  14692  txuni2  14699  txbasex  14700  txbas  14701  txcnp  14714  txcnmpt  14716  txcn  14718  txdis  14720  txdis1cn  14721  cnmpt11  14726  cnmpt12  14730  cnmpt21  14734  cnmpt2t  14736  cnmpt22  14737  blsscls2  14936  xmetxpbl  14951  xmettxlem  14952  tgqioo  14998  fsumcncntop  15010  cncfmpt1f  15041  mulcncflem  15050  mulcncf  15051  dedekindeu  15066  dedekindicclemicc  15075  dedekindicc  15076  ivthinclemdisj  15083  hovercncf  15089  limcimo  15108  cnmptlimc  15117  reldvg  15122  dvfvalap  15124  dvfgg  15131  dvmptfsum  15168  dveflem  15169  dvef  15170  elply2  15178  sincn  15212  coscn  15213  reeff1o  15216  pilem3  15226  ioocosf1o  15297  mpodvdsmulf1o  15433  fsumdvdsmul  15434  perfectlem2  15443  lgsne0  15486  gausslemma2dlem1a  15506  gausslemma2dlem4  15512  lgseisenlem2  15519  lgseisenlem3  15520  lgsquadlem2  15526  2lgslem3  15549  2sqlem2  15563  mul2sq  15564  2sqlem3  15565  2sqlem7  15569  bj-trst  15637  bj-fast  15639  bj-stand  15646  bj-trdc  15650  bj-fadc  15652  decidr  15694  djulclALT  15699  djurclALT  15700  bj-charfunr  15708  bj-indind  15830  bj-2inf  15836  bj-nntrans2  15850  bj-peano4  15853  bj-nnord  15856  bj-inf2vn  15872  bj-inf2vn2  15873  bj-findis  15877  pwf1oexmid  15898  subctctexmid  15899  nnsf  15904  nninfsellemdc  15909  nninffeq  15919  nnnninfen  15920  exmidsbthrlem  15923  sbthom  15927  triap  15930  trilpo  15944  apdifflemr  15948  redcwlpo  15956  tridceq  15957  nconstwlpolem0  15964  nconstwlpolem  15966  nconstwlpo  15967  neapmkv  15969  ltlenmkv  15971