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  mpnanrd  700  oibabs  722  dcim  849  dcstab  852  stdcndc  853  stdcndcOLD  854  dcand  941  dcor  944  dfifp2dc  990  3mix1  1193  3mix2  1194  3jca  1204  syl3anbrc  1208  syl21anbrc  1209  inegd  1417  pclem6  1419  xoranor  1422  dcfrompeirce  1495  nfxfrd  1524  nfd  1572  hban  1596  nfan1  1613  nford  1616  nfand  1617  hbim1  1619  nfal  1625  alexim  1694  nnal  1698  hbn  1699  nf4r  1719  19.34  1732  nfexd  1809  sbcof2  1858  nfsb2or  1885  sbidm  1899  nfdv  1925  nfd2  2075  nfeudv  2094  mon  2108  eumo  2111  mo23  2121  eu2  2124  eu3h  2125  exmodc  2130  exmonim  2131  mo2r  2132  mo3h  2133  bm1.1  2216  eqrdv  2229  3eltr4g  2317  abbi2dv  2351  abbi1dv  2352  nfcd  2370  nfcxfrd  2373  dcned  2409  neqned  2410  3netr4g  2438  necon3bi  2453  necon2ai  2457  nnral  2523  alral  2578  rspe  2582  rsp2e  2584  rgen2a  2587  ralrimi  2604  r19.27v  2661  r19.28v  2662  r19.27av  2669  r19.32r  2680  nfreudxy  2708  mormo  2751  nrexrmo  2756  cgsex2g  2840  cgsex4g  2841  spc2egv  2897  spc2gv  2898  spc3egv  2899  spc3gv  2900  rspce  2906  ceqex  2934  elrab3t  2962  elrabd  2965  mosubt  2984  mo2icl  2986  reu3  2997  reu6i  2998  2rmorex  3013  sbc5  3056  rspesbca  3118  rmo2ilem  3123  sbnfc2  3189  ssrd  3233  ssrdv  3234  3sstr4g  3271  eqsstrid  3274  ss2abdv  3301  abssdv  3302  rabssdv  3308  ss2rabdv  3309  ssun1  3372  unssad  3386  unssbd  3387  ssddif  3443  uneqin  3460  indifdir  3465  undif3ss  3470  reuss2  3489  n0rf  3509  reximdva0m  3512  rabxmdc  3528  ssindif0im  3556  minel  3558  ralidm  3597  ralm  3600  dcun  3606  ifmdc  3652  disjsn2  3736  rabsnif  3742  absneu  3747  rabsneu  3748  opprc  3888  elunii  3903  dfnfc2  3916  uniss2  3929  unidif  3930  ssunieq  3931  intab  3962  iunss2  4020  iunssd  4021  iunxdif2  4024  invdisj  4086  disjiun  4088  3brtr4g  4127  trin  4202  triun  4205  truni  4206  trint  4207  iinexgm  4249  class2seteq  4259  pwuni  4288  exmid1dc  4296  exmidn0m  4297  exmidsssn  4298  exmid0el  4300  exmidel  4301  exmidundif  4302  exmidundifim  4303  exmid1stab  4304  mss  4324  copsex2t  4343  euotd  4353  pwunim  4389  ispod  4407  sotricim  4426  exse  4439  frind  4455  trssord  4483  suctr  4524  pwnex  4552  eusvnf  4556  eusvnfb  4557  eusv2nf  4559  rexxfrd  4566  ralxfr2d  4567  rexxfr2d  4568  rabxfrd  4572  reuhypd  4574  eldifpw  4580  iunpw  4583  ssorduni  4591  onsucb  4607  onsucelsucr  4612  sucunielr  4614  ontriexmidim  4626  ordtri2or2exmidlem  4630  onsucelsucexmid  4634  reg2exmidlema  4638  setindel  4642  elirr  4645  orddisj  4650  en2lp  4658  suc11g  4661  ordsuc  4667  nlimsucg  4670  ordtri2or2exmid  4675  ontri2orexmidim  4676  zfregfr  4678  wessep  4682  tfi  4686  peano5  4702  limom  4718  peano2b  4719  nndceq0  4722  nnpredcl  4727  0nelrel  4778  eqrelrdv  4828  xpsspw  4844  relint  4857  relop  4886  eqbrrdva  4906  ssrelrn  4928  opeldm  4940  reldmm  4956  elres  5055  relssres  5057  elrelimasn  5109  exse2  5117  issref  5126  trin2  5135  dminss  5158  imainss  5159  rnxpid  5178  dmsn0el  5213  dmmptg  5241  relrelss  5270  cnviinm  5285  iotanul  5309  sniota  5324  dffun5r  5345  funmo  5348  funco  5373  funun  5378  fununmo  5379  fununfun  5380  funprg  5387  funtpg  5388  funtp  5390  fntpg  5393  fununi  5405  funcnvuni  5406  imadiflem  5416  imainlem  5418  funimaexglem  5420  isarep2  5424  fnunsn  5446  2elresin  5450  fnimadisj  5460  dmmptd  5470  fco  5507  funssxp  5512  fssres  5520  feu  5527  fimacnvdisj  5529  fabexg  5532  f00  5537  f0rn0  5540  f1co  5563  fores  5578  foco  5579  f1ores  5607  foimacnv  5610  f1oun  5612  fun11iun  5613  f1oco  5615  fo00  5630  brprcneu  5641  fv3  5671  relelfvdm  5680  nfvres  5684  nfunsn  5685  funfvbrb  5769  respreima  5783  dff2  5799  dff3im  5800  dffo4  5803  fvmptelcdm  5808  ffvresb  5818  f1oresrab  5820  fmptco  5821  fsn  5827  fcof  5841  fpr  5844  ftpg  5846  fsnunf  5862  fsnunfv  5863  elabrex  5908  dff1o6  5927  foeqcnvco  5941  fliftel1  5945  isores1  5965  isoini2  5970  riotasbc  5998  acexmidlemph  6021  acexmidlemcase  6023  oprabidlem  6059  brabvv  6077  eloprabga  6118  fnoprabg  6132  caovimo  6226  oprabexd  6298  uchoice  6309  fo1stresm  6333  fo2ndresm  6334  unielxp  6346  1st2ndbr  6356  opabn1stprc  6367  fmpoco  6390  1stconst  6395  2ndconst  6396  poxp  6406  spc2ed  6407  disjxp1  6410  elmpom  6412  suppsnopdc  6428  reldmtpos  6462  tposfun  6469  dftpos4  6472  smores  6501  smores2  6503  tfrlem1  6517  tfr0dm  6531  tfrlemibxssdm  6536  tfrlemibex  6538  tfrlemiubacc  6539  tfrlemi14d  6542  tfrexlem  6543  tfri1d  6544  tfr1onlembxssdm  6552  tfr1onlembex  6554  tfr1onlemubacc  6555  tfr1onlemres  6558  tfrcllemsucfn  6562  tfrcllembxssdm  6565  tfrcllembex  6567  tfrcllemubacc  6568  tfrcllemres  6571  tfri3  6576  rdgon  6595  frecabcl  6608  frecfcllem  6613  frecrdg  6617  2oconcl  6650  nnsucelsuc  6702  nntri3or  6704  nndceq  6710  nndcel  6711  dcdifsnid  6715  ecexr  6750  brdifun  6772  ecelqsdm  6817  iinerm  6819  eroveu  6838  erovlem  6839  ecopovtrn  6844  ecopovtrng  6847  th3qlem1  6849  pmsspw  6895  map0b  6899  mapsn  6902  mapsncnv  6907  ixpf  6932  uniixp  6933  ixpexgg  6934  resixp  6945  f1oen3g  6970  ssdomg  6995  domtr  7002  snfig  7032  modom  7037  enpr2d  7040  dom1o  7045  xpf1o  7073  xpmapenlem  7078  php5dom  7092  fidceq  7099  nnfi  7102  fiunsnnn  7113  findcard  7120  findcard2  7121  findcard2s  7122  ac6sfi  7130  fidcen  7131  tridc  7132  fimax2gtri  7134  finexdc  7135  elssdc  7137  eqsndc  7138  exmidpw  7143  exmidpweq  7144  exmidpw2en  7147  nnwetri  7151  unsnfi  7154  unsnfidcex  7155  unsnfidcel  7156  undifdcss  7158  tpfidisj  7164  tpfidceq  7165  exmidssfi  7174  iunfidisj  7188  snexxph  7192  fidcenumlemrks  7195  sbthlem2  7200  sbthlemi3  7201  sbthlem7  7205  sbthlemi8  7206  fival  7212  dcfi  7223  supmoti  7235  djuss  7312  updjudhf  7321  updjud  7324  casefun  7327  caseinj  7331  omp1eomlem  7336  djufun  7346  djuinj  7348  ctssdccl  7353  ctfoex  7360  nnnninf  7368  nnnninfeq2  7371  nninfisollem0  7372  nninfisollemne  7373  nninfisollemeq  7374  nninfisol  7375  finomni  7382  exmidomniim  7383  exmidomni  7384  fodjuomnilemdc  7386  omniwomnimkv  7409  nninfdcinf  7413  nninfwlporlem  7415  nninfwlpoimlemg  7417  nninfwlpoim  7421  nninfinfwlpo  7422  exmidonfinlem  7447  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  finacn  7462  exmidaclem  7466  dju1en  7471  exmidontriimlem1  7479  exmidontriimlem3  7481  iftrueb01  7484  pw1on  7487  3nsssucpw1  7497  2omotaplemap  7519  2omotap  7521  exmidmotap  7523  cc4f  7531  cc4n  7533  acnccim  7534  dmaddpqlem  7640  nqpi  7641  dmaddpq  7642  dmmulpq  7643  ltdcnq  7660  subhalfnqq  7677  enq0sym  7695  enq0ref  7696  enq0tr  7697  nqnq0pi  7701  nq0nn  7705  addnq0mo  7710  mulnq0mo  7711  nqpnq0nq  7716  nqnq0a  7717  nqnq0m  7718  npsspw  7734  elnp1st2nd  7739  prnmaxl  7751  prnminu  7752  prarloc  7766  genprndl  7784  genprndu  7785  nqprm  7805  nqprl  7814  nqpru  7815  addnqprlemrl  7820  addnqprlemru  7821  prmuloc  7829  mulnqprlemrl  7836  mulnqprlemru  7837  ltsopr  7859  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemopu  7866  lteupri  7880  recexprlemopl  7888  recexprlemopu  7890  recexprlemdisj  7893  archpr  7906  cauappcvgprlemdisj  7914  cauappcvgprlemladdrl  7920  cauappcvgprlem2  7923  caucvgprlemnbj  7930  caucvgprlemdisj  7937  caucvgprlemladdfu  7940  caucvgprlem2  7943  caucvgprprlemnbj  7956  caucvgprprlemdisj  7965  suplocexprlemml  7979  suplocexprlemrl  7980  suplocexprlemmu  7981  suplocexprlemloc  7984  addsrmo  8006  mulsrmo  8007  recexgt0sr  8036  prsrpos  8048  caucvgsrlemasr  8053  suplocsrlemb  8069  suplocsrlempr  8070  suplocsr  8072  elrealeu  8092  pitonn  8111  pitoregt0  8112  pitore  8113  recnnre  8114  axaddcl  8127  axaddrcl  8128  axmulcl  8129  axmulrcl  8130  axrnegex  8142  axcnre  8144  axpre-lttrn  8147  rereceu  8152  axarch  8154  axpre-suploclemres  8164  axpre-suploc  8165  ltxrlt  8287  apirr  8827  divmulasscomap  8918  rerecclap  8952  lbreu  9167  arch  9441  0mnnnnn0  9476  nnm1nn0  9485  elnnnn0c  9489  elnnz1  9546  ztri3or0  9565  nzadd  9576  nn0n0n1ge2  9594  zdceq  9599  zdcle  9600  zdclt  9601  uzind  9635  eluzge3nn  9850  supinfneg  9873  infsupneg  9874  eluz2b2  9881  elnn1uz2  9885  elnn0dc  9889  elnndc  9890  nn01to3  9895  znq  9902  qaddcl  9913  qmulcl  9915  qreccl  9920  irradd  9924  irrmul  9925  elpq  9927  cnref1o  9929  xnn0dcle  10081  xrpnfdc  10121  xrmnfdc  10122  xaddcom  10140  xnegdi  10147  xpncan  10150  xleadd1a  10152  iooidg  10188  elioo4g  10213  elfzd  10296  fzdcel  10320  fznlem  10321  fzpreddisj  10351  fz0to4untppr  10404  elfz0ubfz0  10405  elfz0fzfz0  10406  fz0fzelfz0  10407  fz0fzdiffz0  10410  elfzmlbp  10412  difelfzle  10414  4fvwrd4  10420  fzosplit  10459  elfzo0  10466  nn0p1elfzo  10467  fzo1fzo0n0  10468  elfzonn0  10471  fzofzim  10473  elfzo1  10476  elfzom1elp1fzo  10493  fzossfzop1  10503  ssfzo12bi  10516  exfzdc  10532  zsupcllemstep  10535  infssuzex  10539  qdceq  10550  qdclt  10551  exbtwnzlemstep  10553  exbtwnzlemex  10555  exbtwnz  10556  rebtwn2zlemstep  10558  rebtwn2z  10560  qbtwnxr  10563  modfzo0difsn  10703  frec2uzrand  10713  frec2uzf1od  10714  frecuzrdgrcl  10718  frecuzrdgtcl  10720  frecuzrdgrclt  10723  frecuzrdgfunlem  10727  frecfzennn  10734  nninfinf  10751  seq3f1olemp  10823  seq3f1oleml  10824  seqf1oglem1  10827  ser0f  10842  expcl2lemap  10859  hashunsng  11117  iswrdinn0  11167  snopiswrd  11172  wrdlndm  11179  iswrdsymb  11180  wrdsymb1  11199  ccatfv0  11229  ccatval21sw  11231  lswccatn0lsw  11237  eqs1  11254  ccat1st1st  11267  lswccats1fst  11270  fzowrddc  11277  swrdfv0  11284  swrdlen2  11292  swrdfv2  11293  swrdsbslen  11296  swrdspsleq  11297  pfxfv0  11322  pfxtrcfv0  11324  pfxeq  11326  pfx1  11333  swrdswrdlem  11334  cats1un  11351  pfxccatin12lem2a  11357  pfxccatin12lem2  11361  pfxccatin12lem3  11362  swrdccat  11365  cats1fvn  11394  cats1fvnd  11395  shftfvalg  11441  shftfval  11444  caucvgre  11604  rexanuz  11611  recvguniq  11618  rennim  11625  resqrexlemf  11630  rsqrmo  11650  fimaxre2  11850  climeu  11919  sumdc  11981  summodc  12007  zsumdc  12008  isum  12009  fisumss  12016  isumss2  12017  fsumsplit  12031  sumsnf  12033  fsumsplitsn  12034  sumtp  12038  sumsplitdc  12056  fsum2dlemstep  12058  fisum0diag2  12071  fsumconst  12078  modfsummodlemstep  12081  fsum00  12086  fsumabs  12089  fsumiun  12101  isumlessdc  12120  expcnv  12128  prodmodc  12202  zproddc  12203  iprodap  12204  iprodap0  12206  fprodssdc  12214  prodsnf  12216  fprodsplitdc  12220  fprodsplit  12221  fprodm1  12222  fprod1p  12223  fprodunsn  12228  fprod2dlemstep  12246  fprodsplitsn  12257  ef0lem  12284  modmulconst  12447  dvdsdivcl  12474  dvdsssfz1  12476  dvdsfac  12484  zeoxor  12493  nn0ehalf  12527  nn0oddm1d2  12533  nnoddm1d2  12534  divalglemeunn  12545  divalglemeuneg  12547  bitsfzolem  12578  bitsinv1  12586  gcdsupex  12591  gcdsupcl  12592  bezoutlemnewy  12630  bezoutlemmain  12632  bezoutlemeu  12641  dfgcd2  12648  nnwosdc  12673  nninfct  12675  algrf  12680  algcvgblem  12684  lcmgcdlem  12712  lcmdvds  12714  coprmgcdb  12723  mulgcddvds  12729  qredeu  12732  cncongr1  12738  cncongr2  12739  isprm2lem  12751  dvdsnprmd  12760  prmdc  12765  oddprmge3  12770  pw2dvdseu  12803  phibndlem  12851  dfphi2  12855  hashdvds  12856  phiprmpw  12857  eulerthlemh  12866  hashgcdeq  12875  phisum  12876  odzdvds  12881  reumodprminv  12889  nnnn0modprm0  12891  prm23ge5  12900  pclemdc  12924  pcdvdsb  12956  difsqpwdvds  12974  oddprmdvds  12990  1arith  13003  4sqlem3  13026  4sqlemafi  13031  4sqlemffi  13032  4sqleminfi  13033  4sqexercise1  13034  4sqlem11  13037  4sqlem19  13045  ennnfonelemdc  13083  ennnfonelemh  13088  ennnfonelemhf1o  13097  ennnfonelemf1  13102  ennnfonelemrn  13103  ennnfonelemdm  13104  exmidunben  13110  ctinfomlemom  13111  ctinfom  13112  ctiunctlemudc  13121  ctiunctlemf  13122  ctiunctal  13125  nninfdclemcl  13132  nninfdclemf  13133  nninfdclemp1  13134  isstructim  13159  setsresg  13183  strleund  13249  1strbas  13263  2strbasg  13266  2stropg  13267  restsspw  13395  tgval  13408  ptex  13410  imasaddfnlemg  13460  fnpr2o  13485  fnpr2ob  13486  mgmidsssn0  13530  fngsum  13534  igsumvalx  13535  isnsgrp  13552  sgrpidmndm  13566  mndinvmod  13591  mnd1  13601  mhmeql  13638  grpinveu  13684  prdsinvlem  13754  mulgval  13772  subgintm  13848  trivsubgsnd  13851  eqgfval  13872  ecqusaddd  13888  ecqusaddcl  13889  ghmeql  13917  iscmnd  13948  imasabl  13986  gsumfzmhm2  13994  rnglz  14022  srgfcl  14050  rhmopp  14254  subrgdvds  14313  lssuni  14442  lssintclm  14463  lspf  14468  qusmulrng  14611  mulgrhm2  14689  znf1o  14730  psrbagfi  14753  psrbagconcl  14756  psr1clfi  14772  mplsubgfilemcl  14783  istopon  14807  toponcom  14821  topgele  14823  topontopn  14831  tsettps  14832  eltg2b  14848  unitg  14856  tgss2  14873  bastop2  14878  distop  14879  epttop  14884  cldss2  14900  neisspw  14942  neipsm  14948  neiuni  14955  tgcn  15002  tgcnp  15003  cnntr  15019  lmff  15043  txuni2  15050  txbasex  15051  txbas  15052  txcnp  15065  txcnmpt  15067  txcn  15069  txdis  15071  txdis1cn  15072  cnmpt11  15077  cnmpt12  15081  cnmpt21  15085  cnmpt2t  15087  cnmpt22  15088  blsscls2  15287  xmetxpbl  15302  xmettxlem  15303  tgqioo  15349  fsumcncntop  15361  cncfmpt1f  15392  mulcncflem  15401  mulcncf  15402  dedekindeu  15417  dedekindicclemicc  15426  dedekindicc  15427  ivthinclemdisj  15434  hovercncf  15440  limcimo  15459  cnmptlimc  15468  reldvg  15473  dvfvalap  15475  dvfgg  15482  dvmptfsum  15519  dveflem  15520  dvef  15521  elply2  15529  sincn  15563  coscn  15564  reeff1o  15567  pilem3  15577  ioocosf1o  15648  mpodvdsmulf1o  15787  fsumdvdsmul  15788  perfectlem2  15797  lgsne0  15840  gausslemma2dlem1a  15860  gausslemma2dlem4  15866  lgseisenlem2  15873  lgseisenlem3  15874  lgsquadlem2  15880  2lgslem3  15903  2sqlem2  15917  mul2sq  15918  2sqlem3  15919  2sqlem7  15923  edgstruct  15988  pw0ss  16007  incistruhgr  16014  upgrex  16027  umgrnloop0  16041  upgr1een  16048  lfgrnloopen  16057  umgredg  16069  umgrnloop2  16075  uspgredgiedg  16102  uspgriedgedg  16103  usgrislfuspgrdom  16114  usgredg3  16138  uspgredg2vlem  16144  uspgredg2v  16145  ushgredgedg  16150  ushgredgedgloop  16152  uhgr0vsize0en  16159  usgr1e  16165  subusgr  16199  vtxedgfi  16213  vtxlpfi  16214  vtxdumgrfival  16222  1loopgrvd2fi  16229  p1evtxdeqfilem  16235  vdegp1aid  16238  wlkcprim  16274  wlk1walkdom  16283  uspgr2wlkeq  16289  upgr2wlkdc  16301  wlkres  16303  clwwlkccatlem  16324  clwwlknp  16341  umgr2cwwk2dif  16348  trlsegvdegfi  16391  eupth2lem3lem3fi  16394  eupth2lem3lem6fi  16395  eupth2lem3lem4fi  16397  eupth2lembfi  16401  depindlem1  16430  bj-trst  16440  bj-fast  16442  bj-stand  16449  bj-trdc  16453  bj-fadc  16455  decidr  16497  djulclALT  16502  djurclALT  16503  bj-charfunr  16509  bj-indind  16631  bj-2inf  16637  bj-nntrans2  16651  bj-peano4  16654  bj-nnord  16657  bj-inf2vn  16673  bj-inf2vn2  16674  bj-findis  16678  pwf1oexmid  16704  subctctexmid  16705  pw1dceq  16709  exmidnotnotr  16710  exmidcon  16711  exmidpeirce  16712  nnsf  16714  nninfsellemdc  16719  nninffeq  16729  nnnninfen  16730  exmidsbthrlem  16733  sbthom  16737  triap  16744  trilpo  16758  apdifflemr  16762  redcwlpo  16771  tridceq  16772  nconstwlpolem0  16779  nconstwlpolem  16781  nconstwlpo  16782  neapmkv  16784  ltlenmkv  16786  gfsump1  16798