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  1810  sbcof2  1859  nfsb2or  1886  sbidm  1900  nfdv  1926  nfd2  2076  nfeudv  2095  mon  2109  eumo  2112  mo23  2122  eu2  2125  eu3h  2126  exmodc  2131  exmonim  2132  mo2r  2133  mo3h  2134  bm1.1  2217  eqrdv  2230  3eltr4g  2318  abbi2dv  2353  abbi1dv  2354  nfcd  2379  nfcxfrd  2382  dcned  2418  neqned  2419  3netr4g  2447  necon3bi  2462  necon2ai  2466  nnral  2532  alral  2587  rspe  2591  rsp2e  2593  rgen2a  2596  ralrimi  2613  r19.27v  2670  r19.28v  2671  r19.27av  2678  r19.32r  2689  nfreudxy  2717  mormo  2761  nrexrmo  2766  cgsex2g  2850  cgsex4g  2851  spc2egv  2907  spc2gv  2908  spc3egv  2909  spc3gv  2910  rspce  2916  ceqex  2944  elrab3t  2972  elrabd  2975  mosubt  2994  mo2icl  2996  reu3  3007  reu6i  3008  2rmorex  3023  sbc5  3066  rspesbca  3128  rmo2ilem  3133  sbnfc2  3199  ssrd  3243  ssrdv  3244  3sstr4g  3281  eqsstrid  3284  ss2abdv  3311  abssdv  3312  rabssdv  3318  ss2rabdv  3319  ssun1  3382  unssad  3396  unssbd  3397  ssddif  3455  uneqin  3472  indifdir  3477  undif3ss  3482  reuss2  3501  n0rf  3521  reximdva0m  3524  rabxmdc  3540  ssindif0im  3568  minel  3570  ralidm  3610  ralm  3613  dcun  3619  ifmdc  3665  disjsn2  3752  rabsnif  3758  absneu  3763  rabsneu  3764  opprc  3904  elunii  3919  dfnfc2  3932  uniss2  3945  unidif  3946  ssunieq  3947  intab  3978  iunss2  4036  iunssd  4037  iunxdif2  4040  invdisj  4102  disjiun  4104  3brtr4g  4143  trin  4218  triun  4221  truni  4222  trint  4223  iinexgm  4266  class2seteq  4276  pwuni  4305  exmid1dc  4313  exmidn0m  4314  exmidsssn  4315  exmid0el  4317  exmidel  4318  exmidundif  4319  exmidundifim  4320  exmid1stab  4321  mss  4342  copsex2t  4361  euotd  4371  pwunim  4407  ispod  4425  sotricim  4444  exse  4457  frind  4473  trssord  4501  suctr  4542  pwnex  4570  eusvnf  4574  eusvnfb  4575  eusv2nf  4577  rexxfrd  4584  ralxfr2d  4585  rexxfr2d  4586  rabxfrd  4590  reuhypd  4592  eldifpw  4598  iunpw  4601  ssorduni  4609  onsucb  4625  onsucelsucr  4630  sucunielr  4632  ontriexmidim  4644  ordtri2or2exmidlem  4648  onsucelsucexmid  4652  reg2exmidlema  4656  setindel  4660  elirr  4663  orddisj  4668  en2lp  4676  suc11g  4679  ordsuc  4685  nlimsucg  4688  ordtri2or2exmid  4693  ontri2orexmidim  4694  zfregfr  4696  wessep  4700  tfi  4704  peano5  4720  limom  4736  peano2b  4737  nndceq0  4740  nnpredcl  4745  0nelrel  4796  eqrelrdv  4846  xpsspw  4862  relint  4876  relop  4905  eqbrrdva  4925  ssrelrn  4947  opeldm  4959  reldmm  4975  elres  5074  relssres  5076  elrelimasn  5128  exse2  5136  issref  5145  trin2  5154  dminss  5177  imainss  5178  rnxpid  5197  dmsn0el  5232  dmmptg  5260  relrelss  5289  cnviinm  5304  iotanul  5328  sniota  5343  dffun5r  5364  funmo  5367  funco  5392  funun  5397  fununmo  5398  fununfun  5399  funprg  5406  funtpg  5407  funtp  5409  fntpg  5412  fununi  5424  funcnvuni  5425  imadiflem  5435  imainlem  5437  funimaexglem  5439  isarep2  5443  fnunsn  5465  2elresin  5469  fnimadisj  5479  dmmptd  5489  fco  5527  funssxp  5532  fssres  5540  feu  5549  fimacnvdisj  5551  fabexg  5554  f00  5559  f0rn0  5562  f1co  5585  fores  5600  foco  5601  f1ores  5629  foimacnv  5632  f1oun  5634  fun11iun  5635  f1oco  5637  fo00  5652  brprcneu  5663  fv3  5693  relelfvdm  5702  nfvres  5706  nfunsn  5707  funfvbrb  5791  respreima  5805  dff2  5821  dff3im  5822  dffo4  5825  fvmptelcdm  5830  ffvresb  5840  f1oresrab  5842  fmptco  5843  fsn  5849  fcof  5863  fpr  5866  ftpg  5868  fsnunf  5884  fsnunfv  5885  elabrex  5930  dff1o6  5949  foeqcnvco  5963  fliftel1  5967  isores1  5987  isoini2  5992  riotasbc  6020  acexmidlemph  6043  acexmidlemcase  6045  oprabidlem  6081  brabvv  6099  eloprabga  6140  fnoprabg  6154  caovimo  6248  oprabexd  6320  uchoice  6331  fo1stresm  6355  fo2ndresm  6356  unielxp  6368  1st2ndbr  6378  opabn1stprc  6389  fmpoco  6412  1stconst  6417  2ndconst  6418  poxp  6428  spc2ed  6429  disjxp1  6432  elmpom  6434  suppsnopdc  6450  reldmtpos  6484  tposfun  6491  dftpos4  6494  smores  6523  smores2  6525  tfrlem1  6539  tfr0dm  6553  tfrlemibxssdm  6558  tfrlemibex  6560  tfrlemiubacc  6561  tfrlemi14d  6564  tfrexlem  6565  tfri1d  6566  tfr1onlembxssdm  6574  tfr1onlembex  6576  tfr1onlemubacc  6577  tfr1onlemres  6580  tfrcllemsucfn  6584  tfrcllembxssdm  6587  tfrcllembex  6589  tfrcllemubacc  6590  tfrcllemres  6593  tfri3  6598  rdgon  6617  frecabcl  6630  frecfcllem  6635  frecrdg  6639  2oconcl  6672  nnsucelsuc  6724  nntri3or  6726  nndceq  6732  nndcel  6733  dcdifsnid  6737  ecexr  6772  brdifun  6794  ecelqsdm  6839  iinerm  6841  eroveu  6860  erovlem  6861  ecopovtrn  6866  ecopovtrng  6869  th3qlem1  6871  pmsspw  6917  map0b  6921  mapsnd  6923  mapsn  6925  mapsncnv  6930  ixpf  6955  uniixp  6956  ixpexgg  6957  resixp  6968  f1oen3g  6993  ssdomg  7018  domtr  7025  snfig  7056  modom  7061  enpr2d  7064  dom1o  7069  xpf1o  7097  xpmapenlem  7102  php5dom  7117  fidceq  7124  nnfi  7127  fiunsnnn  7138  findcard  7145  findcard2  7146  findcard2s  7147  ac6sfi  7155  fidcen  7156  tridc  7157  fimax2gtri  7159  finexdc  7160  elssdc  7162  eqsndc  7163  exmidpw  7168  exmidpweq  7169  exmidpw2en  7172  nnwetri  7176  unsnfi  7179  unsnfidcex  7180  unsnfidcel  7181  undifdcss  7183  tpfidisj  7189  tpfidceq  7190  exmidssfi  7199  iunfidisj  7213  mapfi  7214  fissfi  7216  snexxph  7220  fidcenumlemrks  7223  sbthlem2  7228  sbthlemi3  7229  sbthlem7  7233  sbthlemi8  7234  fival  7257  dcfi  7268  supmoti  7284  djuss  7361  updjudhf  7370  updjud  7373  casefun  7376  caseinj  7380  omp1eomlem  7385  djufun  7395  djuinj  7397  ctssdccl  7402  ctfoex  7409  nnnninf  7417  nnnninfeq2  7420  nninfisollem0  7421  nninfisollemne  7422  nninfisollemeq  7423  nninfisol  7424  finomni  7431  exmidomniim  7432  exmidomni  7433  fodjuomnilemdc  7435  omniwomnimkv  7458  nninfdcinf  7462  nninfwlporlem  7464  nninfwlpoimlemg  7466  nninfwlpoim  7470  nninfinfwlpo  7471  exmidonfinlem  7496  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  finacn  7511  exmidaclem  7515  dju1en  7520  exmidontriimlem1  7528  exmidontriimlem3  7530  iftrueb01  7533  pw1on  7536  3nsssucpw1  7546  2omotaplemap  7571  2omotap  7573  exmidmotap  7575  cc4f  7583  cc4n  7585  acnccim  7586  dmaddpqlem  7692  nqpi  7693  dmaddpq  7694  dmmulpq  7695  ltdcnq  7712  subhalfnqq  7729  enq0sym  7747  enq0ref  7748  enq0tr  7749  nqnq0pi  7753  nq0nn  7757  addnq0mo  7762  mulnq0mo  7763  nqpnq0nq  7768  nqnq0a  7769  nqnq0m  7770  npsspw  7786  elnp1st2nd  7791  prnmaxl  7803  prnminu  7804  prarloc  7818  genprndl  7836  genprndu  7837  nqprm  7857  nqprl  7866  nqpru  7867  addnqprlemrl  7872  addnqprlemru  7873  prmuloc  7881  mulnqprlemrl  7888  mulnqprlemru  7889  ltsopr  7911  ltexprlemm  7915  ltexprlemopl  7916  ltexprlemopu  7918  lteupri  7932  recexprlemopl  7940  recexprlemopu  7942  recexprlemdisj  7945  archpr  7958  cauappcvgprlemdisj  7966  cauappcvgprlemladdrl  7972  cauappcvgprlem2  7975  caucvgprlemnbj  7982  caucvgprlemdisj  7989  caucvgprlemladdfu  7992  caucvgprlem2  7995  caucvgprprlemnbj  8008  caucvgprprlemdisj  8017  suplocexprlemml  8031  suplocexprlemrl  8032  suplocexprlemmu  8033  suplocexprlemloc  8036  addsrmo  8058  mulsrmo  8059  recexgt0sr  8088  prsrpos  8100  caucvgsrlemasr  8105  suplocsrlemb  8121  suplocsrlempr  8122  suplocsr  8124  elrealeu  8144  pitonn  8163  pitoregt0  8164  pitore  8165  recnnre  8166  axaddcl  8179  axaddrcl  8180  axmulcl  8181  axmulrcl  8182  axrnegex  8194  axcnre  8196  axpre-lttrn  8199  rereceu  8204  axarch  8206  axpre-suploclemres  8216  axpre-suploc  8217  ltxrlt  8339  apirr  8879  divmulasscomap  8970  rerecclap  9004  lbreu  9219  arch  9493  0mnnnnn0  9528  nnm1nn0  9537  elnnnn0c  9541  elnnz1  9600  ztri3or0  9619  nzadd  9630  nn0n0n1ge2  9648  zdceq  9653  zdcle  9654  zdclt  9655  uzind  9689  eluzge3nn  9904  supinfneg  9927  infsupneg  9928  eluz2b2  9935  elnn1uz2  9939  elnn0dc  9943  elnndc  9944  nn01to3  9949  znq  9956  qaddcl  9967  qmulcl  9969  qreccl  9974  irradd  9978  irrmul  9979  elpq  9981  cnref1o  9983  xnn0dcle  10135  xrpnfdc  10175  xrmnfdc  10176  xaddcom  10194  xnegdi  10201  xpncan  10204  xleadd1a  10206  iooidg  10242  elioo4g  10267  elfzd  10350  fzdcel  10374  fznlem  10375  fzpreddisj  10405  fz0to4untppr  10458  elfz0ubfz0  10459  elfz0fzfz0  10460  fz0fzelfz0  10461  fz0fzdiffz0  10464  elfzmlbp  10466  difelfzle  10468  4fvwrd4  10474  fzosplit  10513  elfzo0  10520  nn0p1elfzo  10521  fzo1fzo0n0  10522  elfzonn0  10525  fzofzim  10527  elfzo1  10530  elfzom1elp1fzo  10547  fzossfzop1  10557  ssfzo12bi  10570  exfzdc  10586  zsupcllemstep  10589  infssuzex  10593  qdceq  10604  qdclt  10605  exbtwnzlemstep  10607  exbtwnzlemex  10609  exbtwnz  10610  rebtwn2zlemstep  10612  rebtwn2z  10614  qbtwnxr  10617  modfzo0difsn  10757  frec2uzrand  10767  frec2uzf1od  10768  frecuzrdgrcl  10772  frecuzrdgtcl  10774  frecuzrdgrclt  10777  frecuzrdgfunlem  10781  frecfzennn  10788  nninfinf  10805  seq3f1olemp  10877  seq3f1oleml  10878  seqf1oglem1  10881  ser0f  10896  expcl2lemap  10913  hashunsng  11172  hashmap  11192  sshashneg  11205  hashfibclem  11206  hashfibc  11207  iswrdinn0  11229  snopiswrd  11234  wrdlndm  11241  iswrdsymb  11242  wrdsymb1  11261  ccatfv0  11291  ccatval21sw  11293  lswccatn0lsw  11299  eqs1  11316  ccat1st1st  11329  lswccats1fst  11332  fzowrddc  11339  swrdfv0  11346  swrdlen2  11354  swrdfv2  11355  swrdsbslen  11358  swrdspsleq  11359  pfxfv0  11384  pfxtrcfv0  11386  pfxeq  11388  pfx1  11395  swrdswrdlem  11396  cats1un  11413  pfxccatin12lem2a  11419  pfxccatin12lem2  11423  pfxccatin12lem3  11424  swrdccat  11427  cats1fvn  11456  cats1fvnd  11457  shftfvalg  11503  shftfval  11506  caucvgre  11666  rexanuz  11673  recvguniq  11680  rennim  11687  resqrexlemf  11692  rsqrmo  11712  fimaxre2  11912  climeu  11981  sumdc  12043  summodc  12069  zsumdc  12070  isum  12071  fisumss  12078  isumss2  12079  fsumsplit  12093  sumsnf  12095  fsumsplitsn  12096  sumtp  12100  sumsplitdc  12118  fsum2dlemstep  12120  fisum0diag2  12133  fsumconst  12140  modfsummodlemstep  12143  fsum00  12148  fsumabs  12151  fsumiun  12163  isumlessdc  12182  expcnv  12190  prodmodc  12264  zproddc  12265  iprodap  12266  iprodap0  12268  fprodssdc  12276  prodsnf  12278  fprodsplitdc  12282  fprodsplit  12283  fprodm1  12284  fprod1p  12285  fprodunsn  12290  fprod2dlemstep  12308  fprodsplitsn  12319  ef0lem  12346  modmulconst  12509  dvdsdivcl  12536  dvdsssfz1  12538  dvdsfac  12546  zeoxor  12555  nn0ehalf  12589  nn0oddm1d2  12595  nnoddm1d2  12596  divalglemeunn  12607  divalglemeuneg  12609  bitsfzolem  12640  bitsinv1  12648  gcdsupex  12653  gcdsupcl  12654  bezoutlemnewy  12692  bezoutlemmain  12694  bezoutlemeu  12703  dfgcd2  12710  nnwosdc  12735  nninfct  12737  algrf  12742  algcvgblem  12746  lcmgcdlem  12774  lcmdvds  12776  coprmgcdb  12785  mulgcddvds  12791  qredeu  12794  cncongr1  12800  cncongr2  12801  isprm2lem  12813  dvdsnprmd  12822  prmdc  12827  oddprmge3  12832  pw2dvdseu  12865  phibndlem  12913  dfphi2  12917  hashdvds  12918  phiprmpw  12919  eulerthlemh  12928  hashgcdeq  12937  phisum  12938  odzdvds  12943  reumodprminv  12951  nnnn0modprm0  12953  prm23ge5  12962  pclemdc  12986  pcdvdsb  13018  difsqpwdvds  13036  oddprmdvds  13052  1arith  13065  4sqlem3  13088  4sqlemafi  13093  4sqlemffi  13094  4sqleminfi  13095  4sqexercise1  13096  4sqlem11  13099  4sqlem19  13107  ballotfilem2  13142  ennnfonelemdc  13150  ennnfonelemh  13155  ennnfonelemhf1o  13164  ennnfonelemf1  13169  ennnfonelemrn  13170  ennnfonelemdm  13171  exmidunben  13177  ctinfomlemom  13178  ctinfom  13179  ctiunctlemudc  13188  ctiunctlemf  13189  ctiunctal  13192  nninfdclemcl  13199  nninfdclemf  13200  nninfdclemp1  13201  isstructim  13226  setsresg  13250  strleund  13316  1strbas  13330  2strbasg  13333  2stropg  13334  restsspw  13462  tgval  13475  ptex  13477  imasaddfnlemg  13527  fnpr2o  13552  fnpr2ob  13553  mgmidsssn0  13597  fngsum  13601  igsumvalx  13602  isnsgrp  13619  sgrpidmndm  13633  mndinvmod  13658  mnd1  13668  mhmeql  13705  grpinveu  13751  prdsinvlem  13821  mulgval  13839  subgintm  13915  trivsubgsnd  13918  eqgfval  13939  ecqusaddd  13955  ecqusaddcl  13956  ghmeql  13984  iscmnd  14015  imasabl  14053  gsumfzmhm2  14061  rnglz  14089  srgfcl  14117  rhmopp  14321  subrgdvds  14380  lssuni  14511  lssintclm  14532  lspf  14537  qusmulrng  14680  mulgrhm2  14758  znf1o  14799  psrbagfi  14823  psrbagconcl  14827  psr1clfi  14843  mplsubgfilemcl  14854  istopon  14878  toponcom  14892  topgele  14894  topontopn  14902  tsettps  14903  eltg2b  14919  unitg  14927  tgss2  14944  bastop2  14949  distop  14950  epttop  14955  cldss2  14971  neisspw  15013  neipsm  15019  neiuni  15026  tgcn  15073  tgcnp  15074  cnntr  15090  lmff  15114  txuni2  15121  txbasex  15122  txbas  15123  txcnp  15136  txcnmpt  15138  txcn  15140  txdis  15142  txdis1cn  15143  cnmpt11  15148  cnmpt12  15152  cnmpt21  15156  cnmpt2t  15158  cnmpt22  15159  blsscls2  15358  xmetxpbl  15373  xmettxlem  15374  tgqioo  15420  fsumcncntop  15432  cncfmpt1f  15463  mulcncflem  15472  mulcncf  15473  dedekindeu  15488  dedekindicclemicc  15497  dedekindicc  15498  ivthinclemdisj  15505  hovercncf  15511  limcimo  15530  cnmptlimc  15539  reldvg  15544  dvfvalap  15546  dvfgg  15553  dvmptfsum  15590  dveflem  15591  dvef  15592  elply2  15600  sincn  15634  coscn  15635  reeff1o  15638  pilem3  15648  ioocosf1o  15719  mpodvdsmulf1o  15858  fsumdvdsmul  15859  perfectlem2  15868  lgsne0  15911  gausslemma2dlem1a  15931  gausslemma2dlem4  15937  lgseisenlem2  15944  lgseisenlem3  15945  lgsquadlem2  15951  2lgslem3  15974  2sqlem2  15988  mul2sq  15989  2sqlem3  15990  2sqlem7  15994  edgstruct  16059  pw0ss  16078  incistruhgr  16085  upgrex  16098  umgrnloop0  16112  upgr1een  16119  lfgrnloopen  16128  umgredg  16140  umgrnloop2  16146  uspgredgiedg  16173  uspgriedgedg  16174  usgrislfuspgrdom  16185  usgredg3  16209  uspgredg2vlem  16215  uspgredg2v  16216  ushgredgedg  16221  ushgredgedgloop  16223  uhgr0vsize0en  16230  usgr1e  16236  subusgr  16270  vtxedgfi  16284  vtxlpfi  16285  vtxdumgrfival  16293  1loopgrvd2fi  16300  p1evtxdeqfilem  16306  vdegp1aid  16309  wlkcprim  16345  wlk1walkdom  16354  uspgr2wlkeq  16360  upgr2wlkdc  16372  wlkres  16374  clwwlkccatlem  16395  clwwlknp  16412  umgr2cwwk2dif  16419  trlsegvdegfi  16462  eupth2lem3lem3fi  16465  eupth2lem3lem6fi  16466  eupth2lem3lem4fi  16468  eupth2lembfi  16472  depindlem1  16501  bj-trst  16511  bj-fast  16513  bj-stand  16520  bj-trdc  16524  bj-fadc  16526  decidr  16568  djulclALT  16573  djurclALT  16574  bj-charfunr  16580  bj-indind  16702  bj-2inf  16708  bj-nntrans2  16722  bj-peano4  16725  bj-nnord  16728  bj-inf2vn  16744  bj-inf2vn2  16745  bj-findis  16749  pwf1oexmid  16773  subctctexmid  16774  pw1dceq  16778  exmidnotnotr  16779  exmidcon  16780  exmidpeirce  16781  nnsf  16783  nninfsellemdc  16788  nninffeq  16798  nnnninfen  16799  exmidsbthrlem  16802  sbthom  16806  triap  16813  trilpo  16827  apdifflemr  16831  redcwlpo  16840  tridceq  16841  nconstwlpolem0  16849  nconstwlpolem  16851  nconstwlpo  16852  neapmkv  16854  ltlenmkv  16856  gfsump1  16868