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  1383  pclem6  1385  xoranor  1388  dcfrompeirce  1460  nfxfrd  1489  nfd  1537  hban  1561  nfan1  1578  nford  1581  nfand  1582  hbim1  1584  nfal  1590  alexim  1659  nnal  1663  ax6blem  1664  nf4r  1685  19.34  1698  nfexd  1775  sbcof2  1824  nfsb2or  1851  sbidm  1865  nfdv  1891  nfd2  2041  nfeudv  2060  mon  2074  eumo  2077  mo23  2086  eu2  2089  eu3h  2090  exmodc  2095  exmonim  2096  mo2r  2097  mo3h  2098  bm1.1  2181  eqrdv  2194  3eltr4g  2282  abbi2dv  2315  abbi1dv  2316  nfcd  2334  nfcxfrd  2337  dcned  2373  neqned  2374  3netr4g  2402  necon3bi  2417  necon2ai  2421  nnral  2487  alral  2542  rspe  2546  rsp2e  2548  rgen2a  2551  ralrimi  2568  r19.27v  2624  r19.28v  2625  r19.27av  2632  r19.32r  2643  nfreudxy  2671  mormo  2713  nrexrmo  2718  cgsex2g  2799  cgsex4g  2800  spc2egv  2854  spc2gv  2855  spc3egv  2856  spc3gv  2857  rspce  2863  ceqex  2891  elrab3t  2919  elrabd  2922  mosubt  2941  mo2icl  2943  reu3  2954  reu6i  2955  2rmorex  2970  sbc5  3013  rspesbca  3074  rmo2ilem  3079  sbnfc2  3145  ssrd  3189  ssrdv  3190  3sstr4g  3227  eqsstrid  3230  ss2abdv  3257  abssdv  3258  rabssdv  3264  ss2rabdv  3265  ssun1  3327  unssad  3341  unssbd  3342  ssddif  3398  uneqin  3415  indifdir  3420  undif3ss  3425  reuss2  3444  n0rf  3464  reximdva0m  3467  rabxmdc  3483  ssindif0im  3511  minel  3513  ralidm  3552  ralm  3555  dcun  3561  ifmdc  3602  disjsn2  3686  absneu  3695  rabsneu  3696  opprc  3830  elunii  3845  dfnfc2  3858  uniss2  3871  unidif  3872  ssunieq  3873  intab  3904  iunss2  3962  iunssd  3963  iunxdif2  3966  invdisj  4028  disjiun  4029  3brtr4g  4068  trin  4142  triun  4145  truni  4146  trint  4147  iinexgm  4188  class2seteq  4197  pwuni  4226  exmid1dc  4234  exmidn0m  4235  exmidsssn  4236  exmid0el  4238  exmidel  4239  exmidundif  4240  exmidundifim  4241  exmid1stab  4242  mss  4260  copsex2t  4279  euotd  4288  pwunim  4322  ispod  4340  sotricim  4359  exse  4372  frind  4388  trssord  4416  suctr  4457  pwnex  4485  eusvnf  4489  eusvnfb  4490  eusv2nf  4492  rexxfrd  4499  ralxfr2d  4500  rexxfr2d  4501  rabxfrd  4505  reuhypd  4507  eldifpw  4513  iunpw  4516  ssorduni  4524  onsucb  4540  onsucelsucr  4545  sucunielr  4547  ontriexmidim  4559  ordtri2or2exmidlem  4563  onsucelsucexmid  4567  reg2exmidlema  4571  setindel  4575  elirr  4578  orddisj  4583  en2lp  4591  suc11g  4594  ordsuc  4600  nlimsucg  4603  ordtri2or2exmid  4608  ontri2orexmidim  4609  zfregfr  4611  wessep  4615  tfi  4619  peano5  4635  limom  4651  peano2b  4652  nndceq0  4655  nnpredcl  4660  0nelrel  4710  eqrelrdv  4760  xpsspw  4776  relint  4788  relop  4817  eqbrrdva  4837  opeldm  4870  elres  4983  relssres  4985  elrelimasn  5036  exse2  5044  issref  5053  trin2  5062  dminss  5085  imainss  5086  rnxpid  5105  dmsn0el  5140  dmmptg  5168  relrelss  5197  cnviinm  5212  iotanul  5235  sniota  5250  dffun5r  5271  funmo  5274  funco  5299  funun  5303  funprg  5309  funtpg  5310  funtp  5312  fntpg  5315  fununi  5327  funcnvuni  5328  imadiflem  5338  imainlem  5340  funimaexglem  5342  isarep2  5346  fnunsn  5368  2elresin  5372  fnimadisj  5381  dmmptd  5391  fco  5426  funssxp  5430  fssres  5436  feu  5443  fimacnvdisj  5445  fabexg  5448  f00  5452  f0rn0  5455  f1co  5478  fores  5493  foco  5494  f1ores  5522  foimacnv  5525  f1oun  5527  fun11iun  5528  f1oco  5530  fo00  5543  brprcneu  5554  fv3  5584  relelfvdm  5593  nfvres  5595  nfunsn  5596  funfvbrb  5678  respreima  5693  dff2  5709  dff3im  5710  dffo4  5713  fvmptelcdm  5718  ffvresb  5728  f1oresrab  5730  fmptco  5731  fsn  5737  fpr  5747  ftpg  5749  fsnunf  5765  fsnunfv  5766  elabrex  5807  dff1o6  5826  foeqcnvco  5840  fliftel1  5844  isores1  5864  isoini2  5869  riotasbc  5896  acexmidlemph  5918  acexmidlemcase  5920  oprabidlem  5956  brabvv  5972  eloprabga  6013  fnoprabg  6027  caovimo  6121  oprabexd  6193  uchoice  6204  fo1stresm  6228  fo2ndresm  6229  unielxp  6241  1st2ndbr  6251  fmpoco  6283  1stconst  6288  2ndconst  6289  poxp  6299  spc2ed  6300  disjxp1  6303  reldmtpos  6320  tposfun  6327  dftpos4  6330  smores  6359  smores2  6361  tfrlem1  6375  tfr0dm  6389  tfrlemibxssdm  6394  tfrlemibex  6396  tfrlemiubacc  6397  tfrlemi14d  6400  tfrexlem  6401  tfri1d  6402  tfr1onlembxssdm  6410  tfr1onlembex  6412  tfr1onlemubacc  6413  tfr1onlemres  6416  tfrcllemsucfn  6420  tfrcllembxssdm  6423  tfrcllembex  6425  tfrcllemubacc  6426  tfrcllemres  6429  tfri3  6434  rdgon  6453  frecabcl  6466  frecfcllem  6471  frecrdg  6475  2oconcl  6506  nnsucelsuc  6558  nntri3or  6560  nndceq  6566  nndcel  6567  dcdifsnid  6571  ecexr  6606  brdifun  6628  ecelqsdm  6673  iinerm  6675  eroveu  6694  erovlem  6695  ecopovtrn  6700  ecopovtrng  6703  th3qlem1  6705  pmsspw  6751  map0b  6755  mapsn  6758  mapsncnv  6763  ixpf  6788  uniixp  6789  ixpexgg  6790  resixp  6801  f1oen3g  6822  ssdomg  6846  domtr  6853  snfig  6882  enpr2d  6885  xpf1o  6914  xpmapenlem  6919  php5dom  6933  fidceq  6939  nnfi  6942  fiunsnnn  6951  findcard  6958  findcard2  6959  findcard2s  6960  ac6sfi  6968  tridc  6969  fimax2gtri  6971  finexdc  6972  exmidpw  6978  exmidpweq  6979  exmidpw2en  6982  nnwetri  6986  unsnfi  6989  unsnfidcex  6990  unsnfidcel  6991  undifdcss  6993  tpfidisj  6999  tpfidceq  7000  iunfidisj  7021  snexxph  7025  fidcenumlemrks  7028  sbthlem2  7033  sbthlemi3  7034  sbthlem7  7038  sbthlemi8  7039  fival  7045  dcfi  7056  supmoti  7068  djuss  7145  updjudhf  7154  updjud  7157  casefun  7160  caseinj  7164  omp1eomlem  7169  djufun  7179  djuinj  7181  ctssdccl  7186  ctfoex  7193  nnnninf  7201  nnnninfeq2  7204  nninfisollem0  7205  nninfisollemne  7206  nninfisollemeq  7207  nninfisol  7208  finomni  7215  exmidomniim  7216  exmidomni  7217  fodjuomnilemdc  7219  omniwomnimkv  7242  nninfdcinf  7246  nninfwlporlem  7248  nninfwlpoimlemg  7250  nninfwlpoim  7253  exmidonfinlem  7272  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  finacn  7287  exmidaclem  7291  dju1en  7296  exmidontriimlem1  7304  exmidontriimlem3  7306  pw1on  7309  3nsssucpw1  7319  2omotaplemap  7340  2omotap  7342  exmidmotap  7344  cc4f  7352  cc4n  7354  acnccim  7355  dmaddpqlem  7461  nqpi  7462  dmaddpq  7463  dmmulpq  7464  ltdcnq  7481  subhalfnqq  7498  enq0sym  7516  enq0ref  7517  enq0tr  7518  nqnq0pi  7522  nq0nn  7526  addnq0mo  7531  mulnq0mo  7532  nqpnq0nq  7537  nqnq0a  7538  nqnq0m  7539  npsspw  7555  elnp1st2nd  7560  prnmaxl  7572  prnminu  7573  prarloc  7587  genprndl  7605  genprndu  7606  nqprm  7626  nqprl  7635  nqpru  7636  addnqprlemrl  7641  addnqprlemru  7642  prmuloc  7650  mulnqprlemrl  7657  mulnqprlemru  7658  ltsopr  7680  ltexprlemm  7684  ltexprlemopl  7685  ltexprlemopu  7687  lteupri  7701  recexprlemopl  7709  recexprlemopu  7711  recexprlemdisj  7714  archpr  7727  cauappcvgprlemdisj  7735  cauappcvgprlemladdrl  7741  cauappcvgprlem2  7744  caucvgprlemnbj  7751  caucvgprlemdisj  7758  caucvgprlemladdfu  7761  caucvgprlem2  7764  caucvgprprlemnbj  7777  caucvgprprlemdisj  7786  suplocexprlemml  7800  suplocexprlemrl  7801  suplocexprlemmu  7802  suplocexprlemloc  7805  addsrmo  7827  mulsrmo  7828  recexgt0sr  7857  prsrpos  7869  caucvgsrlemasr  7874  suplocsrlemb  7890  suplocsrlempr  7891  suplocsr  7893  elrealeu  7913  pitonn  7932  pitoregt0  7933  pitore  7934  recnnre  7935  axaddcl  7948  axaddrcl  7949  axmulcl  7950  axmulrcl  7951  axrnegex  7963  axcnre  7965  axpre-lttrn  7968  rereceu  7973  axarch  7975  axpre-suploclemres  7985  axpre-suploc  7986  ltxrlt  8109  apirr  8649  divmulasscomap  8740  rerecclap  8774  lbreu  8989  arch  9263  0mnnnnn0  9298  nnm1nn0  9307  elnnnn0c  9311  elnnz1  9366  ztri3or0  9385  nzadd  9395  nn0n0n1ge2  9413  zdceq  9418  zdcle  9419  zdclt  9420  uzind  9454  eluzge3nn  9663  supinfneg  9686  infsupneg  9687  eluz2b2  9694  elnn1uz2  9698  elnn0dc  9702  elnndc  9703  nn01to3  9708  znq  9715  qaddcl  9726  qmulcl  9728  qreccl  9733  irradd  9737  irrmul  9738  elpq  9740  cnref1o  9742  xnn0dcle  9894  xrpnfdc  9934  xrmnfdc  9935  xaddcom  9953  xnegdi  9960  xpncan  9963  xleadd1a  9965  iooidg  10001  elioo4g  10026  elfzd  10108  fzdcel  10132  fznlem  10133  fzpreddisj  10163  fz0to4untppr  10216  elfz0ubfz0  10217  elfz0fzfz0  10218  fz0fzelfz0  10219  fz0fzdiffz0  10222  elfzmlbp  10224  difelfzle  10226  4fvwrd4  10232  fzosplit  10270  elfzo0  10275  fzo1fzo0n0  10276  elfzonn0  10279  fzofzim  10281  elfzo1  10283  elfzom1elp1fzo  10295  fzossfzop1  10305  ssfzo12bi  10318  exfzdc  10333  zsupcllemstep  10336  infssuzex  10340  qdceq  10351  qdclt  10352  exbtwnzlemstep  10354  exbtwnzlemex  10356  exbtwnz  10357  rebtwn2zlemstep  10359  rebtwn2z  10361  qbtwnxr  10364  modfzo0difsn  10504  frec2uzrand  10514  frec2uzf1od  10515  frecuzrdgrcl  10519  frecuzrdgtcl  10521  frecuzrdgrclt  10524  frecuzrdgfunlem  10528  frecfzennn  10535  nninfinf  10552  seq3f1olemp  10624  seq3f1oleml  10625  seqf1oglem1  10628  ser0f  10643  expcl2lemap  10660  hashunsng  10916  iswrdinn0  10957  snopiswrd  10962  wrdlndm  10969  iswrdsymb  10970  wrdsymb1  10988  shftfvalg  11000  shftfval  11003  caucvgre  11163  rexanuz  11170  recvguniq  11177  rennim  11184  resqrexlemf  11189  rsqrmo  11209  fimaxre2  11409  climeu  11478  sumdc  11540  summodc  11565  zsumdc  11566  isum  11567  fisumss  11574  isumss2  11575  fsumsplit  11589  sumsnf  11591  fsumsplitsn  11592  sumtp  11596  sumsplitdc  11614  fsum2dlemstep  11616  fisum0diag2  11629  fsumconst  11636  modfsummodlemstep  11639  fsum00  11644  fsumabs  11647  fsumiun  11659  isumlessdc  11678  expcnv  11686  prodmodc  11760  zproddc  11761  iprodap  11762  iprodap0  11764  fprodssdc  11772  prodsnf  11774  fprodsplitdc  11778  fprodsplit  11779  fprodm1  11780  fprod1p  11781  fprodunsn  11786  fprod2dlemstep  11804  fprodsplitsn  11815  ef0lem  11842  modmulconst  12005  dvdsdivcl  12032  dvdsssfz1  12034  dvdsfac  12042  zeoxor  12051  nn0ehalf  12085  nn0oddm1d2  12091  nnoddm1d2  12092  divalglemeunn  12103  divalglemeuneg  12105  bitsfzolem  12136  bitsinv1  12144  gcdsupex  12149  gcdsupcl  12150  bezoutlemnewy  12188  bezoutlemmain  12190  bezoutlemeu  12199  dfgcd2  12206  nnwosdc  12231  nninfct  12233  algrf  12238  algcvgblem  12242  lcmgcdlem  12270  lcmdvds  12272  coprmgcdb  12281  mulgcddvds  12287  qredeu  12290  cncongr1  12296  cncongr2  12297  isprm2lem  12309  dvdsnprmd  12318  prmdc  12323  oddprmge3  12328  pw2dvdseu  12361  phibndlem  12409  dfphi2  12413  hashdvds  12414  phiprmpw  12415  eulerthlemh  12424  hashgcdeq  12433  phisum  12434  odzdvds  12439  reumodprminv  12447  nnnn0modprm0  12449  prm23ge5  12458  pclemdc  12482  pcdvdsb  12514  difsqpwdvds  12532  oddprmdvds  12548  1arith  12561  4sqlem3  12584  4sqlemafi  12589  4sqlemffi  12590  4sqleminfi  12591  4sqexercise1  12592  4sqlem11  12595  4sqlem19  12603  ennnfonelemdc  12641  ennnfonelemh  12646  ennnfonelemhf1o  12655  ennnfonelemf1  12660  ennnfonelemrn  12661  ennnfonelemdm  12662  exmidunben  12668  ctinfomlemom  12669  ctinfom  12670  ctiunctlemudc  12679  ctiunctlemf  12680  ctiunctal  12683  nninfdclemcl  12690  nninfdclemf  12691  nninfdclemp1  12692  isstructim  12717  setsresg  12741  strleund  12806  1strbas  12820  2strbasg  12822  2stropg  12823  restsspw  12951  tgval  12964  ptex  12966  imasaddfnlemg  13016  fnpr2o  13041  fnpr2ob  13042  mgmidsssn0  13086  fngsum  13090  igsumvalx  13091  isnsgrp  13108  sgrpidmndm  13122  mndinvmod  13147  mnd1  13157  mhmeql  13194  grpinveu  13240  prdsinvlem  13310  mulgval  13328  subgintm  13404  trivsubgsnd  13407  eqgfval  13428  ecqusaddd  13444  ecqusaddcl  13445  ghmeql  13473  iscmnd  13504  imasabl  13542  gsumfzmhm2  13550  rnglz  13577  srgfcl  13605  reldvdsrsrg  13724  rhmopp  13808  subrgdvds  13867  lssuni  13995  lssintclm  14016  lspf  14021  qusmulrng  14164  mulgrhm2  14242  znf1o  14283  psr1clfi  14316  istopon  14333  toponcom  14347  topgele  14349  topontopn  14357  tsettps  14358  eltg2b  14374  unitg  14382  tgss2  14399  bastop2  14404  distop  14405  epttop  14410  cldss2  14426  neisspw  14468  neipsm  14474  neiuni  14481  tgcn  14528  tgcnp  14529  cnntr  14545  lmff  14569  txuni2  14576  txbasex  14577  txbas  14578  txcnp  14591  txcnmpt  14593  txcn  14595  txdis  14597  txdis1cn  14598  cnmpt11  14603  cnmpt12  14607  cnmpt21  14611  cnmpt2t  14613  cnmpt22  14614  blsscls2  14813  xmetxpbl  14828  xmettxlem  14829  tgqioo  14875  fsumcncntop  14887  cncfmpt1f  14918  mulcncflem  14927  mulcncf  14928  dedekindeu  14943  dedekindicclemicc  14952  dedekindicc  14953  ivthinclemdisj  14960  hovercncf  14966  limcimo  14985  cnmptlimc  14994  reldvg  14999  dvfvalap  15001  dvfgg  15008  dvmptfsum  15045  dveflem  15046  dvef  15047  elply2  15055  sincn  15089  coscn  15090  reeff1o  15093  pilem3  15103  ioocosf1o  15174  mpodvdsmulf1o  15310  fsumdvdsmul  15311  perfectlem2  15320  lgsne0  15363  gausslemma2dlem1a  15383  gausslemma2dlem4  15389  lgseisenlem2  15396  lgseisenlem3  15397  lgsquadlem2  15403  2lgslem3  15426  2sqlem2  15440  mul2sq  15441  2sqlem3  15442  2sqlem7  15446  bj-trst  15469  bj-fast  15471  bj-stand  15478  bj-trdc  15482  bj-fadc  15484  decidr  15526  djulclALT  15531  djurclALT  15532  bj-charfunr  15540  bj-indind  15662  bj-2inf  15668  bj-nntrans2  15682  bj-peano4  15685  bj-nnord  15688  bj-inf2vn  15704  bj-inf2vn2  15705  bj-findis  15709  pwf1oexmid  15730  subctctexmid  15731  nnsf  15736  nninfsellemdc  15741  nninffeq  15751  nnnninfen  15752  exmidsbthrlem  15753  sbthom  15757  triap  15760  trilpo  15774  apdifflemr  15778  redcwlpo  15786  tridceq  15787  nconstwlpolem0  15794  nconstwlpolem  15796  nconstwlpo  15797  neapmkv  15799  ltlenmkv  15801