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  2836  cgsex4g  2837  spc2egv  2893  spc2gv  2894  spc3egv  2895  spc3gv  2896  rspce  2902  ceqex  2930  elrab3t  2958  elrabd  2961  mosubt  2980  mo2icl  2982  reu3  2993  reu6i  2994  2rmorex  3009  sbc5  3052  rspesbca  3114  rmo2ilem  3119  sbnfc2  3185  ssrd  3229  ssrdv  3230  3sstr4g  3267  eqsstrid  3270  ss2abdv  3297  abssdv  3298  rabssdv  3304  ss2rabdv  3305  ssun1  3367  unssad  3381  unssbd  3382  ssddif  3438  uneqin  3455  indifdir  3460  undif3ss  3465  reuss2  3484  n0rf  3504  reximdva0m  3507  rabxmdc  3523  ssindif0im  3551  minel  3553  ralidm  3592  ralm  3595  dcun  3601  ifmdc  3645  disjsn2  3729  absneu  3738  rabsneu  3739  opprc  3877  elunii  3892  dfnfc2  3905  uniss2  3918  unidif  3919  ssunieq  3920  intab  3951  iunss2  4009  iunssd  4010  iunxdif2  4013  invdisj  4075  disjiun  4077  3brtr4g  4116  trin  4191  triun  4194  truni  4195  trint  4196  iinexgm  4237  class2seteq  4246  pwuni  4275  exmid1dc  4283  exmidn0m  4284  exmidsssn  4285  exmid0el  4287  exmidel  4288  exmidundif  4289  exmidundifim  4290  exmid1stab  4291  mss  4311  copsex2t  4330  euotd  4340  pwunim  4376  ispod  4394  sotricim  4413  exse  4426  frind  4442  trssord  4470  suctr  4511  pwnex  4539  eusvnf  4543  eusvnfb  4544  eusv2nf  4546  rexxfrd  4553  ralxfr2d  4554  rexxfr2d  4555  rabxfrd  4559  reuhypd  4561  eldifpw  4567  iunpw  4570  ssorduni  4578  onsucb  4594  onsucelsucr  4599  sucunielr  4601  ontriexmidim  4613  ordtri2or2exmidlem  4617  onsucelsucexmid  4621  reg2exmidlema  4625  setindel  4629  elirr  4632  orddisj  4637  en2lp  4645  suc11g  4648  ordsuc  4654  nlimsucg  4657  ordtri2or2exmid  4662  ontri2orexmidim  4663  zfregfr  4665  wessep  4669  tfi  4673  peano5  4689  limom  4705  peano2b  4706  nndceq0  4709  nnpredcl  4714  0nelrel  4764  eqrelrdv  4814  xpsspw  4830  relint  4842  relop  4871  eqbrrdva  4891  ssrelrn  4913  opeldm  4925  reldmm  4941  elres  5040  relssres  5042  elrelimasn  5093  exse2  5101  issref  5110  trin2  5119  dminss  5142  imainss  5143  rnxpid  5162  dmsn0el  5197  dmmptg  5225  relrelss  5254  cnviinm  5269  iotanul  5293  sniota  5308  dffun5r  5329  funmo  5332  funco  5357  funun  5361  fununmo  5362  fununfun  5363  funprg  5370  funtpg  5371  funtp  5373  fntpg  5376  fununi  5388  funcnvuni  5389  imadiflem  5399  imainlem  5401  funimaexglem  5403  isarep2  5407  fnunsn  5429  2elresin  5433  fnimadisj  5443  dmmptd  5453  fco  5488  funssxp  5492  fssres  5500  feu  5507  fimacnvdisj  5509  fabexg  5512  f00  5516  f0rn0  5519  f1co  5542  fores  5557  foco  5558  f1ores  5586  foimacnv  5589  f1oun  5591  fun11iun  5592  f1oco  5594  fo00  5608  brprcneu  5619  fv3  5649  relelfvdm  5658  nfvres  5662  nfunsn  5663  funfvbrb  5747  respreima  5762  dff2  5778  dff3im  5779  dffo4  5782  fvmptelcdm  5787  ffvresb  5797  f1oresrab  5799  fmptco  5800  fsn  5806  fpr  5820  ftpg  5822  fsnunf  5838  fsnunfv  5839  elabrex  5880  dff1o6  5899  foeqcnvco  5913  fliftel1  5917  isores1  5937  isoini2  5942  riotasbc  5970  acexmidlemph  5993  acexmidlemcase  5995  oprabidlem  6031  brabvv  6049  eloprabga  6090  fnoprabg  6104  caovimo  6198  oprabexd  6270  uchoice  6281  fo1stresm  6305  fo2ndresm  6306  unielxp  6318  1st2ndbr  6328  fmpoco  6360  1stconst  6365  2ndconst  6366  poxp  6376  spc2ed  6377  disjxp1  6380  reldmtpos  6397  tposfun  6404  dftpos4  6407  smores  6436  smores2  6438  tfrlem1  6452  tfr0dm  6466  tfrlemibxssdm  6471  tfrlemibex  6473  tfrlemiubacc  6474  tfrlemi14d  6477  tfrexlem  6478  tfri1d  6479  tfr1onlembxssdm  6487  tfr1onlembex  6489  tfr1onlemubacc  6490  tfr1onlemres  6493  tfrcllemsucfn  6497  tfrcllembxssdm  6500  tfrcllembex  6502  tfrcllemubacc  6503  tfrcllemres  6506  tfri3  6511  rdgon  6530  frecabcl  6543  frecfcllem  6548  frecrdg  6552  2oconcl  6583  nnsucelsuc  6635  nntri3or  6637  nndceq  6643  nndcel  6644  dcdifsnid  6648  ecexr  6683  brdifun  6705  ecelqsdm  6750  iinerm  6752  eroveu  6771  erovlem  6772  ecopovtrn  6777  ecopovtrng  6780  th3qlem1  6782  pmsspw  6828  map0b  6832  mapsn  6835  mapsncnv  6840  ixpf  6865  uniixp  6866  ixpexgg  6867  resixp  6878  f1oen3g  6903  ssdomg  6928  domtr  6935  snfig  6965  enpr2d  6970  xpf1o  7001  xpmapenlem  7006  php5dom  7020  fidceq  7027  nnfi  7030  fiunsnnn  7039  findcard  7046  findcard2  7047  findcard2s  7048  ac6sfi  7056  tridc  7057  fimax2gtri  7059  finexdc  7060  exmidpw  7066  exmidpweq  7067  exmidpw2en  7070  nnwetri  7074  unsnfi  7077  unsnfidcex  7078  unsnfidcel  7079  undifdcss  7081  tpfidisj  7087  tpfidceq  7088  iunfidisj  7109  snexxph  7113  fidcenumlemrks  7116  sbthlem2  7121  sbthlemi3  7122  sbthlem7  7126  sbthlemi8  7127  fival  7133  dcfi  7144  supmoti  7156  djuss  7233  updjudhf  7242  updjud  7245  casefun  7248  caseinj  7252  omp1eomlem  7257  djufun  7267  djuinj  7269  ctssdccl  7274  ctfoex  7281  nnnninf  7289  nnnninfeq2  7292  nninfisollem0  7293  nninfisollemne  7294  nninfisollemeq  7295  nninfisol  7296  finomni  7303  exmidomniim  7304  exmidomni  7305  fodjuomnilemdc  7307  omniwomnimkv  7330  nninfdcinf  7334  nninfwlporlem  7336  nninfwlpoimlemg  7338  nninfwlpoim  7342  nninfinfwlpo  7343  exmidonfinlem  7367  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  finacn  7382  exmidaclem  7386  dju1en  7391  exmidontriimlem1  7399  exmidontriimlem3  7401  iftrueb01  7404  pw1on  7407  3nsssucpw1  7417  2omotaplemap  7439  2omotap  7441  exmidmotap  7443  cc4f  7451  cc4n  7453  acnccim  7454  dmaddpqlem  7560  nqpi  7561  dmaddpq  7562  dmmulpq  7563  ltdcnq  7580  subhalfnqq  7597  enq0sym  7615  enq0ref  7616  enq0tr  7617  nqnq0pi  7621  nq0nn  7625  addnq0mo  7630  mulnq0mo  7631  nqpnq0nq  7636  nqnq0a  7637  nqnq0m  7638  npsspw  7654  elnp1st2nd  7659  prnmaxl  7671  prnminu  7672  prarloc  7686  genprndl  7704  genprndu  7705  nqprm  7725  nqprl  7734  nqpru  7735  addnqprlemrl  7740  addnqprlemru  7741  prmuloc  7749  mulnqprlemrl  7756  mulnqprlemru  7757  ltsopr  7779  ltexprlemm  7783  ltexprlemopl  7784  ltexprlemopu  7786  lteupri  7800  recexprlemopl  7808  recexprlemopu  7810  recexprlemdisj  7813  archpr  7826  cauappcvgprlemdisj  7834  cauappcvgprlemladdrl  7840  cauappcvgprlem2  7843  caucvgprlemnbj  7850  caucvgprlemdisj  7857  caucvgprlemladdfu  7860  caucvgprlem2  7863  caucvgprprlemnbj  7876  caucvgprprlemdisj  7885  suplocexprlemml  7899  suplocexprlemrl  7900  suplocexprlemmu  7901  suplocexprlemloc  7904  addsrmo  7926  mulsrmo  7927  recexgt0sr  7956  prsrpos  7968  caucvgsrlemasr  7973  suplocsrlemb  7989  suplocsrlempr  7990  suplocsr  7992  elrealeu  8012  pitonn  8031  pitoregt0  8032  pitore  8033  recnnre  8034  axaddcl  8047  axaddrcl  8048  axmulcl  8049  axmulrcl  8050  axrnegex  8062  axcnre  8064  axpre-lttrn  8067  rereceu  8072  axarch  8074  axpre-suploclemres  8084  axpre-suploc  8085  ltxrlt  8208  apirr  8748  divmulasscomap  8839  rerecclap  8873  lbreu  9088  arch  9362  0mnnnnn0  9397  nnm1nn0  9406  elnnnn0c  9410  elnnz1  9465  ztri3or0  9484  nzadd  9495  nn0n0n1ge2  9513  zdceq  9518  zdcle  9519  zdclt  9520  uzind  9554  eluzge3nn  9763  supinfneg  9786  infsupneg  9787  eluz2b2  9794  elnn1uz2  9798  elnn0dc  9802  elnndc  9803  nn01to3  9808  znq  9815  qaddcl  9826  qmulcl  9828  qreccl  9833  irradd  9837  irrmul  9838  elpq  9840  cnref1o  9842  xnn0dcle  9994  xrpnfdc  10034  xrmnfdc  10035  xaddcom  10053  xnegdi  10060  xpncan  10063  xleadd1a  10065  iooidg  10101  elioo4g  10126  elfzd  10208  fzdcel  10232  fznlem  10233  fzpreddisj  10263  fz0to4untppr  10316  elfz0ubfz0  10317  elfz0fzfz0  10318  fz0fzelfz0  10319  fz0fzdiffz0  10322  elfzmlbp  10324  difelfzle  10326  4fvwrd4  10332  fzosplit  10371  elfzo0  10378  fzo1fzo0n0  10379  elfzonn0  10382  fzofzim  10384  elfzo1  10386  elfzom1elp1fzo  10403  fzossfzop1  10413  ssfzo12bi  10426  exfzdc  10441  zsupcllemstep  10444  infssuzex  10448  qdceq  10459  qdclt  10460  exbtwnzlemstep  10462  exbtwnzlemex  10464  exbtwnz  10465  rebtwn2zlemstep  10467  rebtwn2z  10469  qbtwnxr  10472  modfzo0difsn  10612  frec2uzrand  10622  frec2uzf1od  10623  frecuzrdgrcl  10627  frecuzrdgtcl  10629  frecuzrdgrclt  10632  frecuzrdgfunlem  10636  frecfzennn  10643  nninfinf  10660  seq3f1olemp  10732  seq3f1oleml  10733  seqf1oglem1  10736  ser0f  10751  expcl2lemap  10768  hashunsng  11024  iswrdinn0  11071  snopiswrd  11076  wrdlndm  11083  iswrdsymb  11084  wrdsymb1  11103  ccatfv0  11133  ccatval21sw  11135  lswccatn0lsw  11141  eqs1  11156  ccat1st1st  11167  lswccats1fst  11170  fzowrddc  11174  swrdfv0  11181  swrdlen2  11189  swrdfv2  11190  swrdsbslen  11193  swrdspsleq  11194  pfxfv0  11219  pfxtrcfv0  11221  pfxeq  11223  pfx1  11230  swrdswrdlem  11231  cats1un  11248  pfxccatin12lem2a  11254  pfxccatin12lem2  11258  pfxccatin12lem3  11259  swrdccat  11262  cats1fvn  11291  cats1fvnd  11292  shftfvalg  11324  shftfval  11327  caucvgre  11487  rexanuz  11494  recvguniq  11501  rennim  11508  resqrexlemf  11513  rsqrmo  11533  fimaxre2  11733  climeu  11802  sumdc  11864  summodc  11889  zsumdc  11890  isum  11891  fisumss  11898  isumss2  11899  fsumsplit  11913  sumsnf  11915  fsumsplitsn  11916  sumtp  11920  sumsplitdc  11938  fsum2dlemstep  11940  fisum0diag2  11953  fsumconst  11960  modfsummodlemstep  11963  fsum00  11968  fsumabs  11971  fsumiun  11983  isumlessdc  12002  expcnv  12010  prodmodc  12084  zproddc  12085  iprodap  12086  iprodap0  12088  fprodssdc  12096  prodsnf  12098  fprodsplitdc  12102  fprodsplit  12103  fprodm1  12104  fprod1p  12105  fprodunsn  12110  fprod2dlemstep  12128  fprodsplitsn  12139  ef0lem  12166  modmulconst  12329  dvdsdivcl  12356  dvdsssfz1  12358  dvdsfac  12366  zeoxor  12375  nn0ehalf  12409  nn0oddm1d2  12415  nnoddm1d2  12416  divalglemeunn  12427  divalglemeuneg  12429  bitsfzolem  12460  bitsinv1  12468  gcdsupex  12473  gcdsupcl  12474  bezoutlemnewy  12512  bezoutlemmain  12514  bezoutlemeu  12523  dfgcd2  12530  nnwosdc  12555  nninfct  12557  algrf  12562  algcvgblem  12566  lcmgcdlem  12594  lcmdvds  12596  coprmgcdb  12605  mulgcddvds  12611  qredeu  12614  cncongr1  12620  cncongr2  12621  isprm2lem  12633  dvdsnprmd  12642  prmdc  12647  oddprmge3  12652  pw2dvdseu  12685  phibndlem  12733  dfphi2  12737  hashdvds  12738  phiprmpw  12739  eulerthlemh  12748  hashgcdeq  12757  phisum  12758  odzdvds  12763  reumodprminv  12771  nnnn0modprm0  12773  prm23ge5  12782  pclemdc  12806  pcdvdsb  12838  difsqpwdvds  12856  oddprmdvds  12872  1arith  12885  4sqlem3  12908  4sqlemafi  12913  4sqlemffi  12914  4sqleminfi  12915  4sqexercise1  12916  4sqlem11  12919  4sqlem19  12927  ennnfonelemdc  12965  ennnfonelemh  12970  ennnfonelemhf1o  12979  ennnfonelemf1  12984  ennnfonelemrn  12985  ennnfonelemdm  12986  exmidunben  12992  ctinfomlemom  12993  ctinfom  12994  ctiunctlemudc  13003  ctiunctlemf  13004  ctiunctal  13007  nninfdclemcl  13014  nninfdclemf  13015  nninfdclemp1  13016  isstructim  13041  setsresg  13065  strleund  13131  1strbas  13145  2strbasg  13148  2stropg  13149  restsspw  13277  tgval  13290  ptex  13292  imasaddfnlemg  13342  fnpr2o  13367  fnpr2ob  13368  mgmidsssn0  13412  fngsum  13416  igsumvalx  13417  isnsgrp  13434  sgrpidmndm  13448  mndinvmod  13473  mnd1  13483  mhmeql  13520  grpinveu  13566  prdsinvlem  13636  mulgval  13654  subgintm  13730  trivsubgsnd  13733  eqgfval  13754  ecqusaddd  13770  ecqusaddcl  13771  ghmeql  13799  iscmnd  13830  imasabl  13868  gsumfzmhm2  13876  rnglz  13903  srgfcl  13931  reldvdsrsrg  14050  rhmopp  14134  subrgdvds  14193  lssuni  14321  lssintclm  14342  lspf  14347  qusmulrng  14490  mulgrhm2  14568  znf1o  14609  psrbagfi  14631  psr1clfi  14646  mplsubgfilemcl  14657  istopon  14681  toponcom  14695  topgele  14697  topontopn  14705  tsettps  14706  eltg2b  14722  unitg  14730  tgss2  14747  bastop2  14752  distop  14753  epttop  14758  cldss2  14774  neisspw  14816  neipsm  14822  neiuni  14829  tgcn  14876  tgcnp  14877  cnntr  14893  lmff  14917  txuni2  14924  txbasex  14925  txbas  14926  txcnp  14939  txcnmpt  14941  txcn  14943  txdis  14945  txdis1cn  14946  cnmpt11  14951  cnmpt12  14955  cnmpt21  14959  cnmpt2t  14961  cnmpt22  14962  blsscls2  15161  xmetxpbl  15176  xmettxlem  15177  tgqioo  15223  fsumcncntop  15235  cncfmpt1f  15266  mulcncflem  15275  mulcncf  15276  dedekindeu  15291  dedekindicclemicc  15300  dedekindicc  15301  ivthinclemdisj  15308  hovercncf  15314  limcimo  15333  cnmptlimc  15342  reldvg  15347  dvfvalap  15349  dvfgg  15356  dvmptfsum  15393  dveflem  15394  dvef  15395  elply2  15403  sincn  15437  coscn  15438  reeff1o  15441  pilem3  15451  ioocosf1o  15522  mpodvdsmulf1o  15658  fsumdvdsmul  15659  perfectlem2  15668  lgsne0  15711  gausslemma2dlem1a  15731  gausslemma2dlem4  15737  lgseisenlem2  15744  lgseisenlem3  15745  lgsquadlem2  15751  2lgslem3  15774  2sqlem2  15788  mul2sq  15789  2sqlem3  15790  2sqlem7  15794  edgstruct  15858  pw0ss  15877  incistruhgr  15884  upgrex  15897  umgrnloop0  15911  lfgrnloopen  15925  umgredg  15937  umgrnloop2  15943  uspgredgiedg  15970  uspgriedgedg  15971  usgrislfuspgrdom  15982  usgredg3  16006  uspgredg2vlem  16012  uspgredg2v  16013  ushgredgedg  16018  ushgredgedgloop  16020  bj-trst  16061  bj-fast  16063  bj-stand  16070  bj-trdc  16074  bj-fadc  16076  decidr  16118  djulclALT  16123  djurclALT  16124  bj-charfunr  16131  bj-indind  16253  bj-2inf  16259  bj-nntrans2  16273  bj-peano4  16276  bj-nnord  16279  bj-inf2vn  16295  bj-inf2vn2  16296  bj-findis  16300  dom1o  16314  pwf1oexmid  16324  subctctexmid  16325  nnsf  16330  nninfsellemdc  16335  nninffeq  16345  nnnninfen  16346  exmidsbthrlem  16349  sbthom  16353  triap  16356  trilpo  16370  apdifflemr  16374  redcwlpo  16382  tridceq  16383  nconstwlpolem0  16390  nconstwlpolem  16392  nconstwlpo  16393  neapmkv  16395  ltlenmkv  16397