Theorem sylibr 133

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 132	. 2 |- ( ps -> ch )
4	1, 3	syl 14	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbbr  135  pm5.74rd  182  bitri  183  3imtr4i  200  sylanbrc  415  oibabs  709  dcim  836  dcstab  839  stdcndc  840  stdcndcOLD  841  dcor  930  3mix1  1161  3mix2  1162  3jca  1172  syl3anbrc  1176  syl21anbrc  1177  inegd  1367  pclem6  1369  xoranor  1372  nfxfrd  1468  nfd  1516  hban  1540  nfan1  1557  nford  1560  nfand  1561  hbim1  1563  nfal  1569  alexim  1638  nnal  1642  ax6blem  1643  nf4r  1664  19.34  1677  nfexd  1754  sbcof2  1803  nfsb2or  1830  sbidm  1844  nfdv  1870  nfd2  2015  nfeudv  2034  mon  2048  eumo  2051  mo23  2060  eu2  2063  eu3h  2064  exmodc  2069  exmonim  2070  mo2r  2071  mo3h  2072  bm1.1  2155  eqrdv  2168  3eltr4g  2256  abbi2dv  2289  abbi1dv  2290  nfcd  2307  nfcxfrd  2310  dcned  2346  neqned  2347  3netr4g  2375  necon3bi  2390  necon2ai  2394  nnral  2460  alral  2515  rspe  2519  rsp2e  2521  rgen2a  2524  ralrimi  2541  r19.27v  2597  r19.28v  2598  r19.27av  2605  r19.32r  2616  nfreudxy  2643  mormo  2681  nrexrmo  2686  cgsex2g  2766  cgsex4g  2767  spc2egv  2820  spc2gv  2821  spc3egv  2822  spc3gv  2823  rspce  2829  ceqex  2857  elrab3t  2885  elrabd  2888  mosubt  2907  mo2icl  2909  reu3  2920  reu6i  2921  2rmorex  2936  sbc5  2978  rspesbca  3039  rmo2ilem  3044  sbnfc2  3109  ssrd  3152  ssrdv  3153  3sstr4g  3190  eqsstrid  3193  ss2abdv  3220  abssdv  3221  rabssdv  3227  ss2rabdv  3228  ssun1  3290  unssad  3304  unssbd  3305  ssddif  3361  uneqin  3378  indifdir  3383  undif3ss  3388  reuss2  3407  n0rf  3427  reximdva0m  3430  rabxmdc  3446  ssindif0im  3474  minel  3476  ralidm  3515  ralm  3519  dcun  3525  ifmdc  3565  disjsn2  3646  absneu  3655  rabsneu  3656  opprc  3786  elunii  3801  dfnfc2  3814  uniss2  3827  unidif  3828  ssunieq  3829  intab  3860  iunss2  3918  iunxdif2  3921  invdisj  3983  disjiun  3984  3brtr4g  4023  trin  4097  triun  4100  truni  4101  trint  4102  iinexgm  4140  class2seteq  4149  pwuni  4178  exmid1dc  4186  exmidn0m  4187  exmidsssn  4188  exmid0el  4190  exmidel  4191  exmidundif  4192  exmidundifim  4193  mss  4211  copsex2t  4230  euotd  4239  pwunim  4271  ispod  4289  sotricim  4308  exse  4321  frind  4337  trssord  4365  suctr  4406  pwnex  4434  eusvnf  4438  eusvnfb  4439  eusv2nf  4441  rexxfrd  4448  ralxfr2d  4449  rexxfr2d  4450  rabxfrd  4454  reuhypd  4456  eldifpw  4462  iunpw  4465  ssorduni  4471  sucelon  4487  onsucelsucr  4492  sucunielr  4494  ontriexmidim  4506  ordtri2or2exmidlem  4510  onsucelsucexmid  4514  reg2exmidlema  4518  setindel  4522  elirr  4525  orddisj  4530  en2lp  4538  suc11g  4541  ordsuc  4547  nlimsucg  4550  ordtri2or2exmid  4555  ontri2orexmidim  4556  zfregfr  4558  wessep  4562  tfi  4566  peano5  4582  limom  4598  peano2b  4599  nndceq0  4602  nnpredcl  4607  0nelrel  4657  eqrelrdv  4707  xpsspw  4723  relint  4735  relop  4761  eqbrrdva  4781  opeldm  4814  elres  4927  relssres  4929  exse2  4985  issref  4993  trin2  5002  dminss  5025  imainss  5026  rnxpid  5045  dmsn0el  5080  dmmptg  5108  relrelss  5137  cnviinm  5152  iotanul  5175  sniota  5189  dffun5r  5210  funmo  5213  funco  5238  funun  5242  funprg  5248  funtpg  5249  funtp  5251  fntpg  5254  fununi  5266  funcnvuni  5267  imadiflem  5277  imainlem  5279  funimaexglem  5281  isarep2  5285  fnunsn  5305  2elresin  5309  fnimadisj  5318  dmmptd  5328  fco  5363  funssxp  5367  fssres  5373  feu  5380  fimacnvdisj  5382  fabexg  5385  f00  5389  f0rn0  5392  f1co  5415  fores  5429  foco  5430  f1ores  5457  foimacnv  5460  f1oun  5462  fun11iun  5463  f1oco  5465  fo00  5478  brprcneu  5489  fv3  5519  relelfvdm  5528  nfvres  5529  nfunsn  5530  funfvbrb  5609  respreima  5624  dff2  5640  dff3im  5641  dffo4  5644  fvmptelrn  5649  ffvresb  5659  f1oresrab  5661  fmptco  5662  fsn  5668  fpr  5678  ftpg  5680  fsnunf  5696  fsnunfv  5697  elabrex  5737  dff1o6  5755  foeqcnvco  5769  fliftel1  5773  isores1  5793  isoini2  5798  riotasbc  5824  acexmidlemph  5846  acexmidlemcase  5848  oprabidlem  5884  brabvv  5899  eloprabga  5940  fnoprabg  5954  caovimo  6046  oprabexd  6106  fo1stresm  6140  fo2ndresm  6141  unielxp  6153  1st2ndbr  6163  fmpoco  6195  1stconst  6200  2ndconst  6201  poxp  6211  spc2ed  6212  disjxp1  6215  reldmtpos  6232  tposfun  6239  dftpos4  6242  smores  6271  smores2  6273  tfrlem1  6287  tfr0dm  6301  tfrlemibxssdm  6306  tfrlemibex  6308  tfrlemiubacc  6309  tfrlemi14d  6312  tfrexlem  6313  tfri1d  6314  tfr1onlembxssdm  6322  tfr1onlembex  6324  tfr1onlemubacc  6325  tfr1onlemres  6328  tfrcllemsucfn  6332  tfrcllembxssdm  6335  tfrcllembex  6337  tfrcllemubacc  6338  tfrcllemres  6341  tfri3  6346  rdgon  6365  frecabcl  6378  frecfcllem  6383  frecrdg  6387  2oconcl  6418  nnsucelsuc  6470  nntri3or  6472  nndceq  6478  nndcel  6479  dcdifsnid  6483  ecexr  6518  brdifun  6540  ecelqsdm  6583  iinerm  6585  eroveu  6604  erovlem  6605  ecopovtrn  6610  ecopovtrng  6613  th3qlem1  6615  pmsspw  6661  map0b  6665  mapsn  6668  mapsncnv  6673  ixpf  6698  uniixp  6699  ixpexgg  6700  resixp  6711  f1oen3g  6732  ssdomg  6756  domtr  6763  snfig  6792  enpr2d  6795  xpf1o  6822  xpmapenlem  6827  php5dom  6841  fidceq  6847  nnfi  6850  fiunsnnn  6859  findcard  6866  findcard2  6867  findcard2s  6868  ac6sfi  6876  tridc  6877  fimax2gtri  6879  finexdc  6880  exmidpw  6886  exmidpweq  6887  nnwetri  6893  unsnfi  6896  unsnfidcex  6897  unsnfidcel  6898  undifdcss  6900  tpfidisj  6905  iunfidisj  6923  snexxph  6927  fidcenumlemrks  6930  sbthlem2  6935  sbthlemi3  6936  sbthlem7  6940  sbthlemi8  6941  fival  6947  dcfi  6958  supmoti  6970  djuss  7047  updjudhf  7056  updjud  7059  casefun  7062  caseinj  7066  omp1eomlem  7071  djufun  7081  djuinj  7083  ctssdccl  7088  ctfoex  7095  nnnninf  7102  nnnninfeq2  7105  nninfisollem0  7106  nninfisollemne  7107  nninfisollemeq  7108  nninfisol  7109  finomni  7116  exmidomniim  7117  exmidomni  7118  fodjuomnilemdc  7120  omniwomnimkv  7143  nninfdcinf  7147  nninfwlporlem  7149  nninfwlpoimlemg  7151  nninfwlpoim  7154  exmidonfinlem  7170  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidaclem  7185  dju1en  7190  exmidontriimlem1  7198  exmidontriimlem3  7200  pw1on  7203  3nsssucpw1  7213  cc4f  7231  cc4n  7233  dmaddpqlem  7339  nqpi  7340  dmaddpq  7341  dmmulpq  7342  ltdcnq  7359  subhalfnqq  7376  enq0sym  7394  enq0ref  7395  enq0tr  7396  nqnq0pi  7400  nq0nn  7404  addnq0mo  7409  mulnq0mo  7410  nqpnq0nq  7415  nqnq0a  7416  nqnq0m  7417  npsspw  7433  elnp1st2nd  7438  prnmaxl  7450  prnminu  7451  prarloc  7465  genprndl  7483  genprndu  7484  nqprm  7504  nqprl  7513  nqpru  7514  addnqprlemrl  7519  addnqprlemru  7520  prmuloc  7528  mulnqprlemrl  7535  mulnqprlemru  7536  ltsopr  7558  ltexprlemm  7562  ltexprlemopl  7563  ltexprlemopu  7565  lteupri  7579  recexprlemopl  7587  recexprlemopu  7589  recexprlemdisj  7592  archpr  7605  cauappcvgprlemdisj  7613  cauappcvgprlemladdrl  7619  cauappcvgprlem2  7622  caucvgprlemnbj  7629  caucvgprlemdisj  7636  caucvgprlemladdfu  7639  caucvgprlem2  7642  caucvgprprlemnbj  7655  caucvgprprlemdisj  7664  suplocexprlemml  7678  suplocexprlemrl  7679  suplocexprlemmu  7680  suplocexprlemloc  7683  addsrmo  7705  mulsrmo  7706  recexgt0sr  7735  prsrpos  7747  caucvgsrlemasr  7752  suplocsrlemb  7768  suplocsrlempr  7769  suplocsr  7771  elrealeu  7791  pitonn  7810  pitoregt0  7811  pitore  7812  recnnre  7813  axaddcl  7826  axaddrcl  7827  axmulcl  7828  axmulrcl  7829  axrnegex  7841  axcnre  7843  axpre-lttrn  7846  rereceu  7851  axarch  7853  axpre-suploclemres  7863  axpre-suploc  7864  ltxrlt  7985  apirr  8524  divmulasscomap  8613  rerecclap  8647  lbreu  8861  arch  9132  0mnnnnn0  9167  nnm1nn0  9176  elnnnn0c  9180  elnnz1  9235  ztri3or0  9254  nzadd  9264  nn0n0n1ge2  9282  zdceq  9287  zdcle  9288  zdclt  9289  uzind  9323  eluzge3nn  9531  supinfneg  9554  infsupneg  9555  eluz2b2  9562  elnn1uz2  9566  elnn0dc  9570  elnndc  9571  nn01to3  9576  znq  9583  qaddcl  9594  qmulcl  9596  qreccl  9601  irradd  9605  irrmul  9606  elpq  9607  cnref1o  9609  xnn0dcle  9759  xrpnfdc  9799  xrmnfdc  9800  xaddcom  9818  xnegdi  9825  xpncan  9828  xleadd1a  9830  iooidg  9866  elioo4g  9891  fzdcel  9996  fznlem  9997  fzpreddisj  10027  fz0to4untppr  10080  elfz0ubfz0  10081  elfz0fzfz0  10082  fz0fzelfz0  10083  fz0fzdiffz0  10086  elfzmlbp  10088  difelfzle  10090  4fvwrd4  10096  fzosplit  10133  elfzo0  10138  fzo1fzo0n0  10139  elfzonn0  10142  fzofzim  10144  elfzo1  10146  elfzom1elp1fzo  10158  fzossfzop1  10168  ssfzo12bi  10181  exfzdc  10196  qdceq  10203  exbtwnzlemstep  10204  exbtwnzlemex  10206  exbtwnz  10207  rebtwn2zlemstep  10209  rebtwn2z  10211  qbtwnxr  10214  modfzo0difsn  10351  frec2uzrand  10361  frec2uzf1od  10362  frecuzrdgrcl  10366  frecuzrdgtcl  10368  frecuzrdgrclt  10371  frecuzrdgfunlem  10375  frecfzennn  10382  seq3f1olemp  10458  seq3f1oleml  10459  ser0f  10471  expcl2lemap  10488  hashunsng  10742  shftfvalg  10782  shftfval  10785  caucvgre  10945  rexanuz  10952  recvguniq  10959  rennim  10966  resqrexlemf  10971  rsqrmo  10991  fimaxre2  11190  climeu  11259  sumdc  11321  summodc  11346  zsumdc  11347  isum  11348  fisumss  11355  isumss2  11356  fsumsplit  11370  sumsnf  11372  fsumsplitsn  11373  sumtp  11377  sumsplitdc  11395  fsum2dlemstep  11397  fisum0diag2  11410  fsumconst  11417  modfsummodlemstep  11420  fsum00  11425  fsumabs  11428  fsumiun  11440  isumlessdc  11459  expcnv  11467  prodmodc  11541  zproddc  11542  iprodap  11543  iprodap0  11545  fprodssdc  11553  prodsnf  11555  fprodsplitdc  11559  fprodsplit  11560  fprodm1  11561  fprod1p  11562  fprodunsn  11567  fprod2dlemstep  11585  fprodsplitsn  11596  ef0lem  11623  modmulconst  11785  dvdsdivcl  11810  dvdsssfz1  11812  dvdsfac  11820  zeoxor  11828  nn0ehalf  11862  nn0oddm1d2  11868  nnoddm1d2  11869  divalglemeunn  11880  divalglemeuneg  11882  zsupcllemstep  11900  infssuzex  11904  gcdsupex  11912  gcdsupcl  11913  bezoutlemnewy  11951  bezoutlemmain  11953  bezoutlemeu  11962  dfgcd2  11969  nnwosdc  11994  algrf  11999  algcvgblem  12003  lcmgcdlem  12031  lcmdvds  12033  coprmgcdb  12042  mulgcddvds  12048  qredeu  12051  cncongr1  12057  cncongr2  12058  isprm2lem  12070  dvdsnprmd  12079  prmdc  12084  oddprmge3  12089  pw2dvdseu  12122  phibndlem  12170  dfphi2  12174  hashdvds  12175  phiprmpw  12176  eulerthlemh  12185  hashgcdeq  12193  phisum  12194  odzdvds  12199  reumodprminv  12207  nnnn0modprm0  12209  prm23ge5  12218  pclemdc  12242  pcdvdsb  12273  difsqpwdvds  12291  oddprmdvds  12306  1arith  12319  4sqlem3  12342  ennnfonelemdc  12354  ennnfonelemh  12359  ennnfonelemhf1o  12368  ennnfonelemf1  12373  ennnfonelemrn  12374  ennnfonelemdm  12375  exmidunben  12381  ctinfomlemom  12382  ctinfom  12383  ctiunctlemudc  12392  ctiunctlemf  12393  ctiunctal  12396  nninfdclemcl  12403  nninfdclemf  12404  nninfdclemp1  12405  isstructim  12430  setsresg  12454  strleund  12506  1strbas  12517  2strbasg  12519  2stropg  12520  restsspw  12589  mgmidsssn0  12638  isnsgrp  12647  sgrpidmndm  12656  mndinvmod  12678  mnd1  12679  mhmeql  12707  grpinveu  12741  istopon  12805  toponcom  12819  topgele  12821  topontopn  12829  tsettps  12830  tgval  12843  eltg2b  12848  unitg  12856  tgss2  12873  bastop2  12878  distop  12879  epttop  12884  cldss2  12900  neisspw  12942  neipsm  12948  neiuni  12955  tgcn  13002  tgcnp  13003  cnntr  13019  lmff  13043  txuni2  13050  txbasex  13051  txbas  13052  txcnp  13065  txcnmpt  13067  txcn  13069  txdis  13071  txdis1cn  13072  cnmpt11  13077  cnmpt12  13081  cnmpt21  13085  cnmpt2t  13087  cnmpt22  13088  blsscls2  13287  xmetxpbl  13302  xmettxlem  13303  tgqioo  13341  fsumcncntop  13350  cncfmpt1f  13378  mulcncflem  13384  mulcncf  13385  dedekindeu  13395  dedekindicclemicc  13404  dedekindicc  13405  ivthinclemdisj  13412  limcimo  13428  cnmptlimc  13437  reldvg  13442  dvfvalap  13444  dvfgg  13451  dveflem  13481  dvef  13482  sincn  13484  coscn  13485  reeff1o  13488  pilem3  13498  ioocosf1o  13569  lgsne0  13733  2sqlem2  13745  mul2sq  13746  2sqlem3  13747  2sqlem7  13751  bj-trst  13774  bj-fast  13776  bj-stand  13783  bj-trdc  13787  bj-fadc  13789  decidr  13831  djulclALT  13836  djurclALT  13837  bj-charfunr  13845  bj-indind  13967  bj-2inf  13973  bj-nntrans2  13987  bj-peano4  13990  bj-nnord  13993  bj-inf2vn  14009  bj-inf2vn2  14010  bj-findis  14014  pwf1oexmid  14032  exmid1stab  14033  subctctexmid  14034  nnsf  14038  nninfsellemdc  14043  nninffeq  14053  exmidsbthrlem  14054  sbthom  14058  triap  14061  trilpo  14075  apdifflemr  14079  redcwlpo  14087  tridceq  14088  nconstwlpolem0  14094  nconstwlpolem  14096  nconstwlpo  14097  neapmkv  14099