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  697  oibabs  719  dcim  846  dcstab  849  stdcndc  850  stdcndcOLD  851  dcand  938  dcor  941  dfifp2dc  987  3mix1  1190  3mix2  1191  3jca  1201  syl3anbrc  1205  syl21anbrc  1206  inegd  1414  pclem6  1416  xoranor  1419  dcfrompeirce  1492  nfxfrd  1521  nfd  1569  hban  1593  nfan1  1610  nford  1613  nfand  1614  hbim1  1616  nfal  1622  alexim  1691  nnal  1695  ax6blem  1696  nf4r  1717  19.34  1730  nfexd  1807  sbcof2  1856  nfsb2or  1883  sbidm  1897  nfdv  1923  nfd2  2073  nfeudv  2092  mon  2106  eumo  2109  mo23  2119  eu2  2122  eu3h  2123  exmodc  2128  exmonim  2129  mo2r  2130  mo3h  2131  bm1.1  2214  eqrdv  2227  3eltr4g  2315  abbi2dv  2348  abbi1dv  2349  nfcd  2367  nfcxfrd  2370  dcned  2406  neqned  2407  3netr4g  2435  necon3bi  2450  necon2ai  2454  nnral  2520  alral  2575  rspe  2579  rsp2e  2581  rgen2a  2584  ralrimi  2601  r19.27v  2658  r19.28v  2659  r19.27av  2666  r19.32r  2677  nfreudxy  2705  mormo  2748  nrexrmo  2753  cgsex2g  2837  cgsex4g  2838  spc2egv  2894  spc2gv  2895  spc3egv  2896  spc3gv  2897  rspce  2903  ceqex  2931  elrab3t  2959  elrabd  2962  mosubt  2981  mo2icl  2983  reu3  2994  reu6i  2995  2rmorex  3010  sbc5  3053  rspesbca  3115  rmo2ilem  3120  sbnfc2  3186  ssrd  3230  ssrdv  3231  3sstr4g  3268  eqsstrid  3271  ss2abdv  3298  abssdv  3299  rabssdv  3305  ss2rabdv  3306  ssun1  3368  unssad  3382  unssbd  3383  ssddif  3439  uneqin  3456  indifdir  3461  undif3ss  3466  reuss2  3485  n0rf  3505  reximdva0m  3508  rabxmdc  3524  ssindif0im  3552  minel  3554  ralidm  3593  ralm  3596  dcun  3602  ifmdc  3646  disjsn2  3730  rabsnif  3736  absneu  3741  rabsneu  3742  opprc  3881  elunii  3896  dfnfc2  3909  uniss2  3922  unidif  3923  ssunieq  3924  intab  3955  iunss2  4013  iunssd  4014  iunxdif2  4017  invdisj  4079  disjiun  4081  3brtr4g  4120  trin  4195  triun  4198  truni  4199  trint  4200  iinexgm  4242  class2seteq  4251  pwuni  4280  exmid1dc  4288  exmidn0m  4289  exmidsssn  4290  exmid0el  4292  exmidel  4293  exmidundif  4294  exmidundifim  4295  exmid1stab  4296  mss  4316  copsex2t  4335  euotd  4345  pwunim  4381  ispod  4399  sotricim  4418  exse  4431  frind  4447  trssord  4475  suctr  4516  pwnex  4544  eusvnf  4548  eusvnfb  4549  eusv2nf  4551  rexxfrd  4558  ralxfr2d  4559  rexxfr2d  4560  rabxfrd  4564  reuhypd  4566  eldifpw  4572  iunpw  4575  ssorduni  4583  onsucb  4599  onsucelsucr  4604  sucunielr  4606  ontriexmidim  4618  ordtri2or2exmidlem  4622  onsucelsucexmid  4626  reg2exmidlema  4630  setindel  4634  elirr  4637  orddisj  4642  en2lp  4650  suc11g  4653  ordsuc  4659  nlimsucg  4662  ordtri2or2exmid  4667  ontri2orexmidim  4668  zfregfr  4670  wessep  4674  tfi  4678  peano5  4694  limom  4710  peano2b  4711  nndceq0  4714  nnpredcl  4719  0nelrel  4770  eqrelrdv  4820  xpsspw  4836  relint  4849  relop  4878  eqbrrdva  4898  ssrelrn  4920  opeldm  4932  reldmm  4948  elres  5047  relssres  5049  elrelimasn  5100  exse2  5108  issref  5117  trin2  5126  dminss  5149  imainss  5150  rnxpid  5169  dmsn0el  5204  dmmptg  5232  relrelss  5261  cnviinm  5276  iotanul  5300  sniota  5315  dffun5r  5336  funmo  5339  funco  5364  funun  5368  fununmo  5369  fununfun  5370  funprg  5377  funtpg  5378  funtp  5380  fntpg  5383  fununi  5395  funcnvuni  5396  imadiflem  5406  imainlem  5408  funimaexglem  5410  isarep2  5414  fnunsn  5436  2elresin  5440  fnimadisj  5450  dmmptd  5460  fco  5497  funssxp  5501  fssres  5509  feu  5516  fimacnvdisj  5518  fabexg  5521  f00  5525  f0rn0  5528  f1co  5551  fores  5566  foco  5567  f1ores  5595  foimacnv  5598  f1oun  5600  fun11iun  5601  f1oco  5603  fo00  5617  brprcneu  5628  fv3  5658  relelfvdm  5667  nfvres  5671  nfunsn  5672  funfvbrb  5756  respreima  5771  dff2  5787  dff3im  5788  dffo4  5791  fvmptelcdm  5796  ffvresb  5806  f1oresrab  5808  fmptco  5809  fsn  5815  fcof  5828  fpr  5831  ftpg  5833  fsnunf  5849  fsnunfv  5850  elabrex  5893  dff1o6  5912  foeqcnvco  5926  fliftel1  5930  isores1  5950  isoini2  5955  riotasbc  5983  acexmidlemph  6006  acexmidlemcase  6008  oprabidlem  6044  brabvv  6062  eloprabga  6103  fnoprabg  6117  caovimo  6211  oprabexd  6284  uchoice  6295  fo1stresm  6319  fo2ndresm  6320  unielxp  6332  1st2ndbr  6342  opabn1stprc  6353  fmpoco  6376  1stconst  6381  2ndconst  6382  poxp  6392  spc2ed  6393  disjxp1  6396  elmpom  6398  reldmtpos  6414  tposfun  6421  dftpos4  6424  smores  6453  smores2  6455  tfrlem1  6469  tfr0dm  6483  tfrlemibxssdm  6488  tfrlemibex  6490  tfrlemiubacc  6491  tfrlemi14d  6494  tfrexlem  6495  tfri1d  6496  tfr1onlembxssdm  6504  tfr1onlembex  6506  tfr1onlemubacc  6507  tfr1onlemres  6510  tfrcllemsucfn  6514  tfrcllembxssdm  6517  tfrcllembex  6519  tfrcllemubacc  6520  tfrcllemres  6523  tfri3  6528  rdgon  6547  frecabcl  6560  frecfcllem  6565  frecrdg  6569  2oconcl  6602  nnsucelsuc  6654  nntri3or  6656  nndceq  6662  nndcel  6663  dcdifsnid  6667  ecexr  6702  brdifun  6724  ecelqsdm  6769  iinerm  6771  eroveu  6790  erovlem  6791  ecopovtrn  6796  ecopovtrng  6799  th3qlem1  6801  pmsspw  6847  map0b  6851  mapsn  6854  mapsncnv  6859  ixpf  6884  uniixp  6885  ixpexgg  6886  resixp  6897  f1oen3g  6922  ssdomg  6947  domtr  6954  snfig  6984  modom  6989  enpr2d  6992  dom1o  6997  xpf1o  7025  xpmapenlem  7030  php5dom  7044  fidceq  7051  nnfi  7054  fiunsnnn  7063  findcard  7070  findcard2  7071  findcard2s  7072  ac6sfi  7080  fidcen  7081  tridc  7082  fimax2gtri  7084  finexdc  7085  elssdc  7087  eqsndc  7088  exmidpw  7093  exmidpweq  7094  exmidpw2en  7097  nnwetri  7101  unsnfi  7104  unsnfidcex  7105  unsnfidcel  7106  undifdcss  7108  tpfidisj  7114  tpfidceq  7115  iunfidisj  7136  snexxph  7140  fidcenumlemrks  7143  sbthlem2  7148  sbthlemi3  7149  sbthlem7  7153  sbthlemi8  7154  fival  7160  dcfi  7171  supmoti  7183  djuss  7260  updjudhf  7269  updjud  7272  casefun  7275  caseinj  7279  omp1eomlem  7284  djufun  7294  djuinj  7296  ctssdccl  7301  ctfoex  7308  nnnninf  7316  nnnninfeq2  7319  nninfisollem0  7320  nninfisollemne  7321  nninfisollemeq  7322  nninfisol  7323  finomni  7330  exmidomniim  7331  exmidomni  7332  fodjuomnilemdc  7334  omniwomnimkv  7357  nninfdcinf  7361  nninfwlporlem  7363  nninfwlpoimlemg  7365  nninfwlpoim  7369  nninfinfwlpo  7370  exmidonfinlem  7394  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  finacn  7409  exmidaclem  7413  dju1en  7418  exmidontriimlem1  7426  exmidontriimlem3  7428  iftrueb01  7431  pw1on  7434  3nsssucpw1  7444  2omotaplemap  7466  2omotap  7468  exmidmotap  7470  cc4f  7478  cc4n  7480  acnccim  7481  dmaddpqlem  7587  nqpi  7588  dmaddpq  7589  dmmulpq  7590  ltdcnq  7607  subhalfnqq  7624  enq0sym  7642  enq0ref  7643  enq0tr  7644  nqnq0pi  7648  nq0nn  7652  addnq0mo  7657  mulnq0mo  7658  nqpnq0nq  7663  nqnq0a  7664  nqnq0m  7665  npsspw  7681  elnp1st2nd  7686  prnmaxl  7698  prnminu  7699  prarloc  7713  genprndl  7731  genprndu  7732  nqprm  7752  nqprl  7761  nqpru  7762  addnqprlemrl  7767  addnqprlemru  7768  prmuloc  7776  mulnqprlemrl  7783  mulnqprlemru  7784  ltsopr  7806  ltexprlemm  7810  ltexprlemopl  7811  ltexprlemopu  7813  lteupri  7827  recexprlemopl  7835  recexprlemopu  7837  recexprlemdisj  7840  archpr  7853  cauappcvgprlemdisj  7861  cauappcvgprlemladdrl  7867  cauappcvgprlem2  7870  caucvgprlemnbj  7877  caucvgprlemdisj  7884  caucvgprlemladdfu  7887  caucvgprlem2  7890  caucvgprprlemnbj  7903  caucvgprprlemdisj  7912  suplocexprlemml  7926  suplocexprlemrl  7927  suplocexprlemmu  7928  suplocexprlemloc  7931  addsrmo  7953  mulsrmo  7954  recexgt0sr  7983  prsrpos  7995  caucvgsrlemasr  8000  suplocsrlemb  8016  suplocsrlempr  8017  suplocsr  8019  elrealeu  8039  pitonn  8058  pitoregt0  8059  pitore  8060  recnnre  8061  axaddcl  8074  axaddrcl  8075  axmulcl  8076  axmulrcl  8077  axrnegex  8089  axcnre  8091  axpre-lttrn  8094  rereceu  8099  axarch  8101  axpre-suploclemres  8111  axpre-suploc  8112  ltxrlt  8235  apirr  8775  divmulasscomap  8866  rerecclap  8900  lbreu  9115  arch  9389  0mnnnnn0  9424  nnm1nn0  9433  elnnnn0c  9437  elnnz1  9492  ztri3or0  9511  nzadd  9522  nn0n0n1ge2  9540  zdceq  9545  zdcle  9546  zdclt  9547  uzind  9581  eluzge3nn  9796  supinfneg  9819  infsupneg  9820  eluz2b2  9827  elnn1uz2  9831  elnn0dc  9835  elnndc  9836  nn01to3  9841  znq  9848  qaddcl  9859  qmulcl  9861  qreccl  9866  irradd  9870  irrmul  9871  elpq  9873  cnref1o  9875  xnn0dcle  10027  xrpnfdc  10067  xrmnfdc  10068  xaddcom  10086  xnegdi  10093  xpncan  10096  xleadd1a  10098  iooidg  10134  elioo4g  10159  elfzd  10241  fzdcel  10265  fznlem  10266  fzpreddisj  10296  fz0to4untppr  10349  elfz0ubfz0  10350  elfz0fzfz0  10351  fz0fzelfz0  10352  fz0fzdiffz0  10355  elfzmlbp  10357  difelfzle  10359  4fvwrd4  10365  fzosplit  10404  elfzo0  10411  fzo1fzo0n0  10412  elfzonn0  10415  fzofzim  10417  elfzo1  10420  elfzom1elp1fzo  10437  fzossfzop1  10447  ssfzo12bi  10460  exfzdc  10476  zsupcllemstep  10479  infssuzex  10483  qdceq  10494  qdclt  10495  exbtwnzlemstep  10497  exbtwnzlemex  10499  exbtwnz  10500  rebtwn2zlemstep  10502  rebtwn2z  10504  qbtwnxr  10507  modfzo0difsn  10647  frec2uzrand  10657  frec2uzf1od  10658  frecuzrdgrcl  10662  frecuzrdgtcl  10664  frecuzrdgrclt  10667  frecuzrdgfunlem  10671  frecfzennn  10678  nninfinf  10695  seq3f1olemp  10767  seq3f1oleml  10768  seqf1oglem1  10771  ser0f  10786  expcl2lemap  10803  hashunsng  11061  iswrdinn0  11108  snopiswrd  11113  wrdlndm  11120  iswrdsymb  11121  wrdsymb1  11140  ccatfv0  11170  ccatval21sw  11172  lswccatn0lsw  11178  eqs1  11195  ccat1st1st  11208  lswccats1fst  11211  fzowrddc  11218  swrdfv0  11225  swrdlen2  11233  swrdfv2  11234  swrdsbslen  11237  swrdspsleq  11238  pfxfv0  11263  pfxtrcfv0  11265  pfxeq  11267  pfx1  11274  swrdswrdlem  11275  cats1un  11292  pfxccatin12lem2a  11298  pfxccatin12lem2  11302  pfxccatin12lem3  11303  swrdccat  11306  cats1fvn  11335  cats1fvnd  11336  shftfvalg  11369  shftfval  11372  caucvgre  11532  rexanuz  11539  recvguniq  11546  rennim  11553  resqrexlemf  11558  rsqrmo  11578  fimaxre2  11778  climeu  11847  sumdc  11909  summodc  11934  zsumdc  11935  isum  11936  fisumss  11943  isumss2  11944  fsumsplit  11958  sumsnf  11960  fsumsplitsn  11961  sumtp  11965  sumsplitdc  11983  fsum2dlemstep  11985  fisum0diag2  11998  fsumconst  12005  modfsummodlemstep  12008  fsum00  12013  fsumabs  12016  fsumiun  12028  isumlessdc  12047  expcnv  12055  prodmodc  12129  zproddc  12130  iprodap  12131  iprodap0  12133  fprodssdc  12141  prodsnf  12143  fprodsplitdc  12147  fprodsplit  12148  fprodm1  12149  fprod1p  12150  fprodunsn  12155  fprod2dlemstep  12173  fprodsplitsn  12184  ef0lem  12211  modmulconst  12374  dvdsdivcl  12401  dvdsssfz1  12403  dvdsfac  12411  zeoxor  12420  nn0ehalf  12454  nn0oddm1d2  12460  nnoddm1d2  12461  divalglemeunn  12472  divalglemeuneg  12474  bitsfzolem  12505  bitsinv1  12513  gcdsupex  12518  gcdsupcl  12519  bezoutlemnewy  12557  bezoutlemmain  12559  bezoutlemeu  12568  dfgcd2  12575  nnwosdc  12600  nninfct  12602  algrf  12607  algcvgblem  12611  lcmgcdlem  12639  lcmdvds  12641  coprmgcdb  12650  mulgcddvds  12656  qredeu  12659  cncongr1  12665  cncongr2  12666  isprm2lem  12678  dvdsnprmd  12687  prmdc  12692  oddprmge3  12697  pw2dvdseu  12730  phibndlem  12778  dfphi2  12782  hashdvds  12783  phiprmpw  12784  eulerthlemh  12793  hashgcdeq  12802  phisum  12803  odzdvds  12808  reumodprminv  12816  nnnn0modprm0  12818  prm23ge5  12827  pclemdc  12851  pcdvdsb  12883  difsqpwdvds  12901  oddprmdvds  12917  1arith  12930  4sqlem3  12953  4sqlemafi  12958  4sqlemffi  12959  4sqleminfi  12960  4sqexercise1  12961  4sqlem11  12964  4sqlem19  12972  ennnfonelemdc  13010  ennnfonelemh  13015  ennnfonelemhf1o  13024  ennnfonelemf1  13029  ennnfonelemrn  13030  ennnfonelemdm  13031  exmidunben  13037  ctinfomlemom  13038  ctinfom  13039  ctiunctlemudc  13048  ctiunctlemf  13049  ctiunctal  13052  nninfdclemcl  13059  nninfdclemf  13060  nninfdclemp1  13061  isstructim  13086  setsresg  13110  strleund  13176  1strbas  13190  2strbasg  13193  2stropg  13194  restsspw  13322  tgval  13335  ptex  13337  imasaddfnlemg  13387  fnpr2o  13412  fnpr2ob  13413  mgmidsssn0  13457  fngsum  13461  igsumvalx  13462  isnsgrp  13479  sgrpidmndm  13493  mndinvmod  13518  mnd1  13528  mhmeql  13565  grpinveu  13611  prdsinvlem  13681  mulgval  13699  subgintm  13775  trivsubgsnd  13778  eqgfval  13799  ecqusaddd  13815  ecqusaddcl  13816  ghmeql  13844  iscmnd  13875  imasabl  13913  gsumfzmhm2  13921  rnglz  13948  srgfcl  13976  rhmopp  14180  subrgdvds  14239  lssuni  14367  lssintclm  14388  lspf  14393  qusmulrng  14536  mulgrhm2  14614  znf1o  14655  psrbagfi  14677  psr1clfi  14692  mplsubgfilemcl  14703  istopon  14727  toponcom  14741  topgele  14743  topontopn  14751  tsettps  14752  eltg2b  14768  unitg  14776  tgss2  14793  bastop2  14798  distop  14799  epttop  14804  cldss2  14820  neisspw  14862  neipsm  14868  neiuni  14875  tgcn  14922  tgcnp  14923  cnntr  14939  lmff  14963  txuni2  14970  txbasex  14971  txbas  14972  txcnp  14985  txcnmpt  14987  txcn  14989  txdis  14991  txdis1cn  14992  cnmpt11  14997  cnmpt12  15001  cnmpt21  15005  cnmpt2t  15007  cnmpt22  15008  blsscls2  15207  xmetxpbl  15222  xmettxlem  15223  tgqioo  15269  fsumcncntop  15281  cncfmpt1f  15312  mulcncflem  15321  mulcncf  15322  dedekindeu  15337  dedekindicclemicc  15346  dedekindicc  15347  ivthinclemdisj  15354  hovercncf  15360  limcimo  15379  cnmptlimc  15388  reldvg  15393  dvfvalap  15395  dvfgg  15402  dvmptfsum  15439  dveflem  15440  dvef  15441  elply2  15449  sincn  15483  coscn  15484  reeff1o  15487  pilem3  15497  ioocosf1o  15568  mpodvdsmulf1o  15704  fsumdvdsmul  15705  perfectlem2  15714  lgsne0  15757  gausslemma2dlem1a  15777  gausslemma2dlem4  15783  lgseisenlem2  15790  lgseisenlem3  15791  lgsquadlem2  15797  2lgslem3  15820  2sqlem2  15834  mul2sq  15835  2sqlem3  15836  2sqlem7  15840  edgstruct  15905  pw0ss  15924  incistruhgr  15931  upgrex  15944  umgrnloop0  15958  lfgrnloopen  15972  umgredg  15984  umgrnloop2  15990  uspgredgiedg  16017  uspgriedgedg  16018  usgrislfuspgrdom  16029  usgredg3  16053  uspgredg2vlem  16059  uspgredg2v  16060  ushgredgedg  16065  ushgredgedgloop  16067  uhgr0vsize0en  16074  usgr1e  16080  vtxedgfi  16095  vtxlpfi  16096  vtxdumgrfival  16104  1loopgrvd2fi  16111  wlkcprim  16147  wlk1walkdom  16156  uspgr2wlkeq  16162  upgr2wlkdc  16172  wlkres  16174  clwwlkccatlem  16195  clwwlknp  16212  umgr2cwwk2dif  16219  bj-trst  16271  bj-fast  16273  bj-stand  16280  bj-trdc  16284  bj-fadc  16286  decidr  16328  djulclALT  16333  djurclALT  16334  bj-charfunr  16341  bj-indind  16463  bj-2inf  16469  bj-nntrans2  16483  bj-peano4  16486  bj-nnord  16489  bj-inf2vn  16505  bj-inf2vn2  16506  bj-findis  16510  pwf1oexmid  16536  subctctexmid  16537  pw1dceq  16541  nnsf  16543  nninfsellemdc  16548  nninffeq  16558  nnnninfen  16559  exmidsbthrlem  16562  sbthom  16566  triap  16569  trilpo  16583  apdifflemr  16587  redcwlpo  16595  tridceq  16596  nconstwlpolem0  16603  nconstwlpolem  16605  nconstwlpo  16606  neapmkv  16608  ltlenmkv  16610