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  3878  elunii  3893  dfnfc2  3906  uniss2  3919  unidif  3920  ssunieq  3921  intab  3952  iunss2  4010  iunssd  4011  iunxdif2  4014  invdisj  4076  disjiun  4078  3brtr4g  4117  trin  4192  triun  4195  truni  4196  trint  4197  iinexgm  4238  class2seteq  4247  pwuni  4276  exmid1dc  4284  exmidn0m  4285  exmidsssn  4286  exmid0el  4288  exmidel  4289  exmidundif  4290  exmidundifim  4291  exmid1stab  4292  mss  4312  copsex2t  4331  euotd  4341  pwunim  4377  ispod  4395  sotricim  4414  exse  4427  frind  4443  trssord  4471  suctr  4512  pwnex  4540  eusvnf  4544  eusvnfb  4545  eusv2nf  4547  rexxfrd  4554  ralxfr2d  4555  rexxfr2d  4556  rabxfrd  4560  reuhypd  4562  eldifpw  4568  iunpw  4571  ssorduni  4579  onsucb  4595  onsucelsucr  4600  sucunielr  4602  ontriexmidim  4614  ordtri2or2exmidlem  4618  onsucelsucexmid  4622  reg2exmidlema  4626  setindel  4630  elirr  4633  orddisj  4638  en2lp  4646  suc11g  4649  ordsuc  4655  nlimsucg  4658  ordtri2or2exmid  4663  ontri2orexmidim  4664  zfregfr  4666  wessep  4670  tfi  4674  peano5  4690  limom  4706  peano2b  4707  nndceq0  4710  nnpredcl  4715  0nelrel  4765  eqrelrdv  4815  xpsspw  4831  relint  4843  relop  4872  eqbrrdva  4892  ssrelrn  4914  opeldm  4926  reldmm  4942  elres  5041  relssres  5043  elrelimasn  5094  exse2  5102  issref  5111  trin2  5120  dminss  5143  imainss  5144  rnxpid  5163  dmsn0el  5198  dmmptg  5226  relrelss  5255  cnviinm  5270  iotanul  5294  sniota  5309  dffun5r  5330  funmo  5333  funco  5358  funun  5362  fununmo  5363  fununfun  5364  funprg  5371  funtpg  5372  funtp  5374  fntpg  5377  fununi  5389  funcnvuni  5390  imadiflem  5400  imainlem  5402  funimaexglem  5404  isarep2  5408  fnunsn  5430  2elresin  5434  fnimadisj  5444  dmmptd  5454  fco  5491  funssxp  5495  fssres  5503  feu  5510  fimacnvdisj  5512  fabexg  5515  f00  5519  f0rn0  5522  f1co  5545  fores  5560  foco  5561  f1ores  5589  foimacnv  5592  f1oun  5594  fun11iun  5595  f1oco  5597  fo00  5611  brprcneu  5622  fv3  5652  relelfvdm  5661  nfvres  5665  nfunsn  5666  funfvbrb  5750  respreima  5765  dff2  5781  dff3im  5782  dffo4  5785  fvmptelcdm  5790  ffvresb  5800  f1oresrab  5802  fmptco  5803  fsn  5809  fcof  5822  fpr  5825  ftpg  5827  fsnunf  5843  fsnunfv  5844  elabrex  5887  dff1o6  5906  foeqcnvco  5920  fliftel1  5924  isores1  5944  isoini2  5949  riotasbc  5977  acexmidlemph  6000  acexmidlemcase  6002  oprabidlem  6038  brabvv  6056  eloprabga  6097  fnoprabg  6111  caovimo  6205  oprabexd  6278  uchoice  6289  fo1stresm  6313  fo2ndresm  6314  unielxp  6326  1st2ndbr  6336  fmpoco  6368  1stconst  6373  2ndconst  6374  poxp  6384  spc2ed  6385  disjxp1  6388  reldmtpos  6405  tposfun  6412  dftpos4  6415  smores  6444  smores2  6446  tfrlem1  6460  tfr0dm  6474  tfrlemibxssdm  6479  tfrlemibex  6481  tfrlemiubacc  6482  tfrlemi14d  6485  tfrexlem  6486  tfri1d  6487  tfr1onlembxssdm  6495  tfr1onlembex  6497  tfr1onlemubacc  6498  tfr1onlemres  6501  tfrcllemsucfn  6505  tfrcllembxssdm  6508  tfrcllembex  6510  tfrcllemubacc  6511  tfrcllemres  6514  tfri3  6519  rdgon  6538  frecabcl  6551  frecfcllem  6556  frecrdg  6560  2oconcl  6593  nnsucelsuc  6645  nntri3or  6647  nndceq  6653  nndcel  6654  dcdifsnid  6658  ecexr  6693  brdifun  6715  ecelqsdm  6760  iinerm  6762  eroveu  6781  erovlem  6782  ecopovtrn  6787  ecopovtrng  6790  th3qlem1  6792  pmsspw  6838  map0b  6842  mapsn  6845  mapsncnv  6850  ixpf  6875  uniixp  6876  ixpexgg  6877  resixp  6888  f1oen3g  6913  ssdomg  6938  domtr  6945  snfig  6975  enpr2d  6980  dom1o  6985  xpf1o  7013  xpmapenlem  7018  php5dom  7032  fidceq  7039  nnfi  7042  fiunsnnn  7051  findcard  7058  findcard2  7059  findcard2s  7060  ac6sfi  7068  fidcen  7069  tridc  7070  fimax2gtri  7072  finexdc  7073  elssdc  7075  eqsndc  7076  exmidpw  7081  exmidpweq  7082  exmidpw2en  7085  nnwetri  7089  unsnfi  7092  unsnfidcex  7093  unsnfidcel  7094  undifdcss  7096  tpfidisj  7102  tpfidceq  7103  iunfidisj  7124  snexxph  7128  fidcenumlemrks  7131  sbthlem2  7136  sbthlemi3  7137  sbthlem7  7141  sbthlemi8  7142  fival  7148  dcfi  7159  supmoti  7171  djuss  7248  updjudhf  7257  updjud  7260  casefun  7263  caseinj  7267  omp1eomlem  7272  djufun  7282  djuinj  7284  ctssdccl  7289  ctfoex  7296  nnnninf  7304  nnnninfeq2  7307  nninfisollem0  7308  nninfisollemne  7309  nninfisollemeq  7310  nninfisol  7311  finomni  7318  exmidomniim  7319  exmidomni  7320  fodjuomnilemdc  7322  omniwomnimkv  7345  nninfdcinf  7349  nninfwlporlem  7351  nninfwlpoimlemg  7353  nninfwlpoim  7357  nninfinfwlpo  7358  exmidonfinlem  7382  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  finacn  7397  exmidaclem  7401  dju1en  7406  exmidontriimlem1  7414  exmidontriimlem3  7416  iftrueb01  7419  pw1on  7422  3nsssucpw1  7432  2omotaplemap  7454  2omotap  7456  exmidmotap  7458  cc4f  7466  cc4n  7468  acnccim  7469  dmaddpqlem  7575  nqpi  7576  dmaddpq  7577  dmmulpq  7578  ltdcnq  7595  subhalfnqq  7612  enq0sym  7630  enq0ref  7631  enq0tr  7632  nqnq0pi  7636  nq0nn  7640  addnq0mo  7645  mulnq0mo  7646  nqpnq0nq  7651  nqnq0a  7652  nqnq0m  7653  npsspw  7669  elnp1st2nd  7674  prnmaxl  7686  prnminu  7687  prarloc  7701  genprndl  7719  genprndu  7720  nqprm  7740  nqprl  7749  nqpru  7750  addnqprlemrl  7755  addnqprlemru  7756  prmuloc  7764  mulnqprlemrl  7771  mulnqprlemru  7772  ltsopr  7794  ltexprlemm  7798  ltexprlemopl  7799  ltexprlemopu  7801  lteupri  7815  recexprlemopl  7823  recexprlemopu  7825  recexprlemdisj  7828  archpr  7841  cauappcvgprlemdisj  7849  cauappcvgprlemladdrl  7855  cauappcvgprlem2  7858  caucvgprlemnbj  7865  caucvgprlemdisj  7872  caucvgprlemladdfu  7875  caucvgprlem2  7878  caucvgprprlemnbj  7891  caucvgprprlemdisj  7900  suplocexprlemml  7914  suplocexprlemrl  7915  suplocexprlemmu  7916  suplocexprlemloc  7919  addsrmo  7941  mulsrmo  7942  recexgt0sr  7971  prsrpos  7983  caucvgsrlemasr  7988  suplocsrlemb  8004  suplocsrlempr  8005  suplocsr  8007  elrealeu  8027  pitonn  8046  pitoregt0  8047  pitore  8048  recnnre  8049  axaddcl  8062  axaddrcl  8063  axmulcl  8064  axmulrcl  8065  axrnegex  8077  axcnre  8079  axpre-lttrn  8082  rereceu  8087  axarch  8089  axpre-suploclemres  8099  axpre-suploc  8100  ltxrlt  8223  apirr  8763  divmulasscomap  8854  rerecclap  8888  lbreu  9103  arch  9377  0mnnnnn0  9412  nnm1nn0  9421  elnnnn0c  9425  elnnz1  9480  ztri3or0  9499  nzadd  9510  nn0n0n1ge2  9528  zdceq  9533  zdcle  9534  zdclt  9535  uzind  9569  eluzge3nn  9779  supinfneg  9802  infsupneg  9803  eluz2b2  9810  elnn1uz2  9814  elnn0dc  9818  elnndc  9819  nn01to3  9824  znq  9831  qaddcl  9842  qmulcl  9844  qreccl  9849  irradd  9853  irrmul  9854  elpq  9856  cnref1o  9858  xnn0dcle  10010  xrpnfdc  10050  xrmnfdc  10051  xaddcom  10069  xnegdi  10076  xpncan  10079  xleadd1a  10081  iooidg  10117  elioo4g  10142  elfzd  10224  fzdcel  10248  fznlem  10249  fzpreddisj  10279  fz0to4untppr  10332  elfz0ubfz0  10333  elfz0fzfz0  10334  fz0fzelfz0  10335  fz0fzdiffz0  10338  elfzmlbp  10340  difelfzle  10342  4fvwrd4  10348  fzosplit  10387  elfzo0  10394  fzo1fzo0n0  10395  elfzonn0  10398  fzofzim  10400  elfzo1  10403  elfzom1elp1fzo  10420  fzossfzop1  10430  ssfzo12bi  10443  exfzdc  10458  zsupcllemstep  10461  infssuzex  10465  qdceq  10476  qdclt  10477  exbtwnzlemstep  10479  exbtwnzlemex  10481  exbtwnz  10482  rebtwn2zlemstep  10484  rebtwn2z  10486  qbtwnxr  10489  modfzo0difsn  10629  frec2uzrand  10639  frec2uzf1od  10640  frecuzrdgrcl  10644  frecuzrdgtcl  10646  frecuzrdgrclt  10649  frecuzrdgfunlem  10653  frecfzennn  10660  nninfinf  10677  seq3f1olemp  10749  seq3f1oleml  10750  seqf1oglem1  10753  ser0f  10768  expcl2lemap  10785  hashunsng  11042  iswrdinn0  11089  snopiswrd  11094  wrdlndm  11101  iswrdsymb  11102  wrdsymb1  11121  ccatfv0  11151  ccatval21sw  11153  lswccatn0lsw  11159  eqs1  11176  ccat1st1st  11187  lswccats1fst  11190  fzowrddc  11194  swrdfv0  11201  swrdlen2  11209  swrdfv2  11210  swrdsbslen  11213  swrdspsleq  11214  pfxfv0  11239  pfxtrcfv0  11241  pfxeq  11243  pfx1  11250  swrdswrdlem  11251  cats1un  11268  pfxccatin12lem2a  11274  pfxccatin12lem2  11278  pfxccatin12lem3  11279  swrdccat  11282  cats1fvn  11311  cats1fvnd  11312  shftfvalg  11344  shftfval  11347  caucvgre  11507  rexanuz  11514  recvguniq  11521  rennim  11528  resqrexlemf  11533  rsqrmo  11553  fimaxre2  11753  climeu  11822  sumdc  11884  summodc  11909  zsumdc  11910  isum  11911  fisumss  11918  isumss2  11919  fsumsplit  11933  sumsnf  11935  fsumsplitsn  11936  sumtp  11940  sumsplitdc  11958  fsum2dlemstep  11960  fisum0diag2  11973  fsumconst  11980  modfsummodlemstep  11983  fsum00  11988  fsumabs  11991  fsumiun  12003  isumlessdc  12022  expcnv  12030  prodmodc  12104  zproddc  12105  iprodap  12106  iprodap0  12108  fprodssdc  12116  prodsnf  12118  fprodsplitdc  12122  fprodsplit  12123  fprodm1  12124  fprod1p  12125  fprodunsn  12130  fprod2dlemstep  12148  fprodsplitsn  12159  ef0lem  12186  modmulconst  12349  dvdsdivcl  12376  dvdsssfz1  12378  dvdsfac  12386  zeoxor  12395  nn0ehalf  12429  nn0oddm1d2  12435  nnoddm1d2  12436  divalglemeunn  12447  divalglemeuneg  12449  bitsfzolem  12480  bitsinv1  12488  gcdsupex  12493  gcdsupcl  12494  bezoutlemnewy  12532  bezoutlemmain  12534  bezoutlemeu  12543  dfgcd2  12550  nnwosdc  12575  nninfct  12577  algrf  12582  algcvgblem  12586  lcmgcdlem  12614  lcmdvds  12616  coprmgcdb  12625  mulgcddvds  12631  qredeu  12634  cncongr1  12640  cncongr2  12641  isprm2lem  12653  dvdsnprmd  12662  prmdc  12667  oddprmge3  12672  pw2dvdseu  12705  phibndlem  12753  dfphi2  12757  hashdvds  12758  phiprmpw  12759  eulerthlemh  12768  hashgcdeq  12777  phisum  12778  odzdvds  12783  reumodprminv  12791  nnnn0modprm0  12793  prm23ge5  12802  pclemdc  12826  pcdvdsb  12858  difsqpwdvds  12876  oddprmdvds  12892  1arith  12905  4sqlem3  12928  4sqlemafi  12933  4sqlemffi  12934  4sqleminfi  12935  4sqexercise1  12936  4sqlem11  12939  4sqlem19  12947  ennnfonelemdc  12985  ennnfonelemh  12990  ennnfonelemhf1o  12999  ennnfonelemf1  13004  ennnfonelemrn  13005  ennnfonelemdm  13006  exmidunben  13012  ctinfomlemom  13013  ctinfom  13014  ctiunctlemudc  13023  ctiunctlemf  13024  ctiunctal  13027  nninfdclemcl  13034  nninfdclemf  13035  nninfdclemp1  13036  isstructim  13061  setsresg  13085  strleund  13151  1strbas  13165  2strbasg  13168  2stropg  13169  restsspw  13297  tgval  13310  ptex  13312  imasaddfnlemg  13362  fnpr2o  13387  fnpr2ob  13388  mgmidsssn0  13432  fngsum  13436  igsumvalx  13437  isnsgrp  13454  sgrpidmndm  13468  mndinvmod  13493  mnd1  13503  mhmeql  13540  grpinveu  13586  prdsinvlem  13656  mulgval  13674  subgintm  13750  trivsubgsnd  13753  eqgfval  13774  ecqusaddd  13790  ecqusaddcl  13791  ghmeql  13819  iscmnd  13850  imasabl  13888  gsumfzmhm2  13896  rnglz  13923  srgfcl  13951  rhmopp  14155  subrgdvds  14214  lssuni  14342  lssintclm  14363  lspf  14368  qusmulrng  14511  mulgrhm2  14589  znf1o  14630  psrbagfi  14652  psr1clfi  14667  mplsubgfilemcl  14678  istopon  14702  toponcom  14716  topgele  14718  topontopn  14726  tsettps  14727  eltg2b  14743  unitg  14751  tgss2  14768  bastop2  14773  distop  14774  epttop  14779  cldss2  14795  neisspw  14837  neipsm  14843  neiuni  14850  tgcn  14897  tgcnp  14898  cnntr  14914  lmff  14938  txuni2  14945  txbasex  14946  txbas  14947  txcnp  14960  txcnmpt  14962  txcn  14964  txdis  14966  txdis1cn  14967  cnmpt11  14972  cnmpt12  14976  cnmpt21  14980  cnmpt2t  14982  cnmpt22  14983  blsscls2  15182  xmetxpbl  15197  xmettxlem  15198  tgqioo  15244  fsumcncntop  15256  cncfmpt1f  15287  mulcncflem  15296  mulcncf  15297  dedekindeu  15312  dedekindicclemicc  15321  dedekindicc  15322  ivthinclemdisj  15329  hovercncf  15335  limcimo  15354  cnmptlimc  15363  reldvg  15368  dvfvalap  15370  dvfgg  15377  dvmptfsum  15414  dveflem  15415  dvef  15416  elply2  15424  sincn  15458  coscn  15459  reeff1o  15462  pilem3  15472  ioocosf1o  15543  mpodvdsmulf1o  15679  fsumdvdsmul  15680  perfectlem2  15689  lgsne0  15732  gausslemma2dlem1a  15752  gausslemma2dlem4  15758  lgseisenlem2  15765  lgseisenlem3  15766  lgsquadlem2  15772  2lgslem3  15795  2sqlem2  15809  mul2sq  15810  2sqlem3  15811  2sqlem7  15815  edgstruct  15879  pw0ss  15898  incistruhgr  15905  upgrex  15918  umgrnloop0  15932  lfgrnloopen  15946  umgredg  15958  umgrnloop2  15964  uspgredgiedg  15991  uspgriedgedg  15992  usgrislfuspgrdom  16003  usgredg3  16027  uspgredg2vlem  16033  uspgredg2v  16034  ushgredgedg  16039  ushgredgedgloop  16041  vtxedgfi  16048  vtxlpfi  16049  vtxdumgrfival  16057  wlkcprim  16091  wlk1walkdom  16100  uspgr2wlkeq  16106  upgr2wlkdc  16116  wlkres  16118  clwwlkccatlem  16137  bj-trst  16158  bj-fast  16160  bj-stand  16167  bj-trdc  16171  bj-fadc  16173  decidr  16215  djulclALT  16220  djurclALT  16221  bj-charfunr  16228  bj-indind  16350  bj-2inf  16356  bj-nntrans2  16370  bj-peano4  16373  bj-nnord  16376  bj-inf2vn  16392  bj-inf2vn2  16393  bj-findis  16397  pwf1oexmid  16424  subctctexmid  16425  pw1dceq  16429  nnsf  16431  nninfsellemdc  16436  nninffeq  16446  nnnninfen  16447  exmidsbthrlem  16450  sbthom  16454  triap  16457  trilpo  16471  apdifflemr  16475  redcwlpo  16483  tridceq  16484  nconstwlpolem0  16491  nconstwlpolem  16493  nconstwlpo  16494  neapmkv  16496  ltlenmkv  16498