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  shftfvalg  11071  shftfval  11074  caucvgre  11234  rexanuz  11241  recvguniq  11248  rennim  11255  resqrexlemf  11260  rsqrmo  11280  fimaxre2  11480  climeu  11549  sumdc  11611  summodc  11636  zsumdc  11637  isum  11638  fisumss  11645  isumss2  11646  fsumsplit  11660  sumsnf  11662  fsumsplitsn  11663  sumtp  11667  sumsplitdc  11685  fsum2dlemstep  11687  fisum0diag2  11700  fsumconst  11707  modfsummodlemstep  11710  fsum00  11715  fsumabs  11718  fsumiun  11730  isumlessdc  11749  expcnv  11757  prodmodc  11831  zproddc  11832  iprodap  11833  iprodap0  11835  fprodssdc  11843  prodsnf  11845  fprodsplitdc  11849  fprodsplit  11850  fprodm1  11851  fprod1p  11852  fprodunsn  11857  fprod2dlemstep  11875  fprodsplitsn  11886  ef0lem  11913  modmulconst  12076  dvdsdivcl  12103  dvdsssfz1  12105  dvdsfac  12113  zeoxor  12122  nn0ehalf  12156  nn0oddm1d2  12162  nnoddm1d2  12163  divalglemeunn  12174  divalglemeuneg  12176  bitsfzolem  12207  bitsinv1  12215  gcdsupex  12220  gcdsupcl  12221  bezoutlemnewy  12259  bezoutlemmain  12261  bezoutlemeu  12270  dfgcd2  12277  nnwosdc  12302  nninfct  12304  algrf  12309  algcvgblem  12313  lcmgcdlem  12341  lcmdvds  12343  coprmgcdb  12352  mulgcddvds  12358  qredeu  12361  cncongr1  12367  cncongr2  12368  isprm2lem  12380  dvdsnprmd  12389  prmdc  12394  oddprmge3  12399  pw2dvdseu  12432  phibndlem  12480  dfphi2  12484  hashdvds  12485  phiprmpw  12486  eulerthlemh  12495  hashgcdeq  12504  phisum  12505  odzdvds  12510  reumodprminv  12518  nnnn0modprm0  12520  prm23ge5  12529  pclemdc  12553  pcdvdsb  12585  difsqpwdvds  12603  oddprmdvds  12619  1arith  12632  4sqlem3  12655  4sqlemafi  12660  4sqlemffi  12661  4sqleminfi  12662  4sqexercise1  12663  4sqlem11  12666  4sqlem19  12674  ennnfonelemdc  12712  ennnfonelemh  12717  ennnfonelemhf1o  12726  ennnfonelemf1  12731  ennnfonelemrn  12732  ennnfonelemdm  12733  exmidunben  12739  ctinfomlemom  12740  ctinfom  12741  ctiunctlemudc  12750  ctiunctlemf  12751  ctiunctal  12754  nninfdclemcl  12761  nninfdclemf  12762  nninfdclemp1  12763  isstructim  12788  setsresg  12812  strleund  12877  1strbas  12891  2strbasg  12894  2stropg  12895  restsspw  13023  tgval  13036  ptex  13038  imasaddfnlemg  13088  fnpr2o  13113  fnpr2ob  13114  mgmidsssn0  13158  fngsum  13162  igsumvalx  13163  isnsgrp  13180  sgrpidmndm  13194  mndinvmod  13219  mnd1  13229  mhmeql  13266  grpinveu  13312  prdsinvlem  13382  mulgval  13400  subgintm  13476  trivsubgsnd  13479  eqgfval  13500  ecqusaddd  13516  ecqusaddcl  13517  ghmeql  13545  iscmnd  13576  imasabl  13614  gsumfzmhm2  13622  rnglz  13649  srgfcl  13677  reldvdsrsrg  13796  rhmopp  13880  subrgdvds  13939  lssuni  14067  lssintclm  14088  lspf  14093  qusmulrng  14236  mulgrhm2  14314  znf1o  14355  psrbagfi  14377  psr1clfi  14392  mplsubgfilemcl  14403  istopon  14427  toponcom  14441  topgele  14443  topontopn  14451  tsettps  14452  eltg2b  14468  unitg  14476  tgss2  14493  bastop2  14498  distop  14499  epttop  14504  cldss2  14520  neisspw  14562  neipsm  14568  neiuni  14575  tgcn  14622  tgcnp  14623  cnntr  14639  lmff  14663  txuni2  14670  txbasex  14671  txbas  14672  txcnp  14685  txcnmpt  14687  txcn  14689  txdis  14691  txdis1cn  14692  cnmpt11  14697  cnmpt12  14701  cnmpt21  14705  cnmpt2t  14707  cnmpt22  14708  blsscls2  14907  xmetxpbl  14922  xmettxlem  14923  tgqioo  14969  fsumcncntop  14981  cncfmpt1f  15012  mulcncflem  15021  mulcncf  15022  dedekindeu  15037  dedekindicclemicc  15046  dedekindicc  15047  ivthinclemdisj  15054  hovercncf  15060  limcimo  15079  cnmptlimc  15088  reldvg  15093  dvfvalap  15095  dvfgg  15102  dvmptfsum  15139  dveflem  15140  dvef  15141  elply2  15149  sincn  15183  coscn  15184  reeff1o  15187  pilem3  15197  ioocosf1o  15268  mpodvdsmulf1o  15404  fsumdvdsmul  15405  perfectlem2  15414  lgsne0  15457  gausslemma2dlem1a  15477  gausslemma2dlem4  15483  lgseisenlem2  15490  lgseisenlem3  15491  lgsquadlem2  15497  2lgslem3  15520  2sqlem2  15534  mul2sq  15535  2sqlem3  15536  2sqlem7  15540  bj-trst  15608  bj-fast  15610  bj-stand  15617  bj-trdc  15621  bj-fadc  15623  decidr  15665  djulclALT  15670  djurclALT  15671  bj-charfunr  15679  bj-indind  15801  bj-2inf  15807  bj-nntrans2  15821  bj-peano4  15824  bj-nnord  15827  bj-inf2vn  15843  bj-inf2vn2  15844  bj-findis  15848  pwf1oexmid  15869  subctctexmid  15870  nnsf  15875  nninfsellemdc  15880  nninffeq  15890  nnnninfen  15891  exmidsbthrlem  15894  sbthom  15898  triap  15901  trilpo  15915  apdifflemr  15919  redcwlpo  15927  tridceq  15928  nconstwlpolem0  15935  nconstwlpolem  15937  nconstwlpo  15938  neapmkv  15940  ltlenmkv  15942