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  714  dcim  841  dcstab  844  stdcndc  845  stdcndcOLD  846  dcor  935  3mix1  1166  3mix2  1167  3jca  1177  syl3anbrc  1181  syl21anbrc  1182  inegd  1372  pclem6  1374  xoranor  1377  nfxfrd  1475  nfd  1523  hban  1547  nfan1  1564  nford  1567  nfand  1568  hbim1  1570  nfal  1576  alexim  1645  nnal  1649  ax6blem  1650  nf4r  1671  19.34  1684  nfexd  1761  sbcof2  1810  nfsb2or  1837  sbidm  1851  nfdv  1877  nfd2  2022  nfeudv  2041  mon  2055  eumo  2058  mo23  2067  eu2  2070  eu3h  2071  exmodc  2076  exmonim  2077  mo2r  2078  mo3h  2079  bm1.1  2162  eqrdv  2175  3eltr4g  2263  abbi2dv  2296  abbi1dv  2297  nfcd  2314  nfcxfrd  2317  dcned  2353  neqned  2354  3netr4g  2382  necon3bi  2397  necon2ai  2401  nnral  2467  alral  2522  rspe  2526  rsp2e  2528  rgen2a  2531  ralrimi  2548  r19.27v  2604  r19.28v  2605  r19.27av  2612  r19.32r  2623  nfreudxy  2650  mormo  2688  nrexrmo  2693  cgsex2g  2773  cgsex4g  2774  spc2egv  2827  spc2gv  2828  spc3egv  2829  spc3gv  2830  rspce  2836  ceqex  2864  elrab3t  2892  elrabd  2895  mosubt  2914  mo2icl  2916  reu3  2927  reu6i  2928  2rmorex  2943  sbc5  2986  rspesbca  3047  rmo2ilem  3052  sbnfc2  3117  ssrd  3160  ssrdv  3161  3sstr4g  3198  eqsstrid  3201  ss2abdv  3228  abssdv  3229  rabssdv  3235  ss2rabdv  3236  ssun1  3298  unssad  3312  unssbd  3313  ssddif  3369  uneqin  3386  indifdir  3391  undif3ss  3396  reuss2  3415  n0rf  3435  reximdva0m  3438  rabxmdc  3454  ssindif0im  3482  minel  3484  ralidm  3523  ralm  3527  dcun  3533  ifmdc  3574  disjsn2  3655  absneu  3664  rabsneu  3665  opprc  3799  elunii  3814  dfnfc2  3827  uniss2  3840  unidif  3841  ssunieq  3842  intab  3873  iunss2  3931  iunssd  3932  iunxdif2  3935  invdisj  3997  disjiun  3998  3brtr4g  4037  trin  4111  triun  4114  truni  4115  trint  4116  iinexgm  4154  class2seteq  4163  pwuni  4192  exmid1dc  4200  exmidn0m  4201  exmidsssn  4202  exmid0el  4204  exmidel  4205  exmidundif  4206  exmidundifim  4207  exmid1stab  4208  mss  4226  copsex2t  4245  euotd  4254  pwunim  4286  ispod  4304  sotricim  4323  exse  4336  frind  4352  trssord  4380  suctr  4421  pwnex  4449  eusvnf  4453  eusvnfb  4454  eusv2nf  4456  rexxfrd  4463  ralxfr2d  4464  rexxfr2d  4465  rabxfrd  4469  reuhypd  4471  eldifpw  4477  iunpw  4480  ssorduni  4486  onsucb  4502  onsucelsucr  4507  sucunielr  4509  ontriexmidim  4521  ordtri2or2exmidlem  4525  onsucelsucexmid  4529  reg2exmidlema  4533  setindel  4537  elirr  4540  orddisj  4545  en2lp  4553  suc11g  4556  ordsuc  4562  nlimsucg  4565  ordtri2or2exmid  4570  ontri2orexmidim  4571  zfregfr  4573  wessep  4577  tfi  4581  peano5  4597  limom  4613  peano2b  4614  nndceq0  4617  nnpredcl  4622  0nelrel  4672  eqrelrdv  4722  xpsspw  4738  relint  4750  relop  4777  eqbrrdva  4797  opeldm  4830  elres  4943  relssres  4945  elrelimasn  4994  exse2  5002  issref  5011  trin2  5020  dminss  5043  imainss  5044  rnxpid  5063  dmsn0el  5098  dmmptg  5126  relrelss  5155  cnviinm  5170  iotanul  5193  sniota  5207  dffun5r  5228  funmo  5231  funco  5256  funun  5260  funprg  5266  funtpg  5267  funtp  5269  fntpg  5272  fununi  5284  funcnvuni  5285  imadiflem  5295  imainlem  5297  funimaexglem  5299  isarep2  5303  fnunsn  5323  2elresin  5327  fnimadisj  5336  dmmptd  5346  fco  5381  funssxp  5385  fssres  5391  feu  5398  fimacnvdisj  5400  fabexg  5403  f00  5407  f0rn0  5410  f1co  5433  fores  5447  foco  5448  f1ores  5476  foimacnv  5479  f1oun  5481  fun11iun  5482  f1oco  5484  fo00  5497  brprcneu  5508  fv3  5538  relelfvdm  5547  nfvres  5548  nfunsn  5549  funfvbrb  5629  respreima  5644  dff2  5660  dff3im  5661  dffo4  5664  fvmptelcdm  5669  ffvresb  5679  f1oresrab  5681  fmptco  5682  fsn  5688  fpr  5698  ftpg  5700  fsnunf  5716  fsnunfv  5717  elabrex  5758  dff1o6  5776  foeqcnvco  5790  fliftel1  5794  isores1  5814  isoini2  5819  riotasbc  5845  acexmidlemph  5867  acexmidlemcase  5869  oprabidlem  5905  brabvv  5920  eloprabga  5961  fnoprabg  5975  caovimo  6067  oprabexd  6127  fo1stresm  6161  fo2ndresm  6162  unielxp  6174  1st2ndbr  6184  fmpoco  6216  1stconst  6221  2ndconst  6222  poxp  6232  spc2ed  6233  disjxp1  6236  reldmtpos  6253  tposfun  6260  dftpos4  6263  smores  6292  smores2  6294  tfrlem1  6308  tfr0dm  6322  tfrlemibxssdm  6327  tfrlemibex  6329  tfrlemiubacc  6330  tfrlemi14d  6333  tfrexlem  6334  tfri1d  6335  tfr1onlembxssdm  6343  tfr1onlembex  6345  tfr1onlemubacc  6346  tfr1onlemres  6349  tfrcllemsucfn  6353  tfrcllembxssdm  6356  tfrcllembex  6358  tfrcllemubacc  6359  tfrcllemres  6362  tfri3  6367  rdgon  6386  frecabcl  6399  frecfcllem  6404  frecrdg  6408  2oconcl  6439  nnsucelsuc  6491  nntri3or  6493  nndceq  6499  nndcel  6500  dcdifsnid  6504  ecexr  6539  brdifun  6561  ecelqsdm  6604  iinerm  6606  eroveu  6625  erovlem  6626  ecopovtrn  6631  ecopovtrng  6634  th3qlem1  6636  pmsspw  6682  map0b  6686  mapsn  6689  mapsncnv  6694  ixpf  6719  uniixp  6720  ixpexgg  6721  resixp  6732  f1oen3g  6753  ssdomg  6777  domtr  6784  snfig  6813  enpr2d  6816  xpf1o  6843  xpmapenlem  6848  php5dom  6862  fidceq  6868  nnfi  6871  fiunsnnn  6880  findcard  6887  findcard2  6888  findcard2s  6889  ac6sfi  6897  tridc  6898  fimax2gtri  6900  finexdc  6901  exmidpw  6907  exmidpweq  6908  nnwetri  6914  unsnfi  6917  unsnfidcex  6918  unsnfidcel  6919  undifdcss  6921  tpfidisj  6926  iunfidisj  6944  snexxph  6948  fidcenumlemrks  6951  sbthlem2  6956  sbthlemi3  6957  sbthlem7  6961  sbthlemi8  6962  fival  6968  dcfi  6979  supmoti  6991  djuss  7068  updjudhf  7077  updjud  7080  casefun  7083  caseinj  7087  omp1eomlem  7092  djufun  7102  djuinj  7104  ctssdccl  7109  ctfoex  7116  nnnninf  7123  nnnninfeq2  7126  nninfisollem0  7127  nninfisollemne  7128  nninfisollemeq  7129  nninfisol  7130  finomni  7137  exmidomniim  7138  exmidomni  7139  fodjuomnilemdc  7141  omniwomnimkv  7164  nninfdcinf  7168  nninfwlporlem  7170  nninfwlpoimlemg  7172  nninfwlpoim  7175  exmidonfinlem  7191  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  exmidaclem  7206  dju1en  7211  exmidontriimlem1  7219  exmidontriimlem3  7221  pw1on  7224  3nsssucpw1  7234  2omotaplemap  7255  2omotap  7257  exmidmotap  7259  cc4f  7267  cc4n  7269  dmaddpqlem  7375  nqpi  7376  dmaddpq  7377  dmmulpq  7378  ltdcnq  7395  subhalfnqq  7412  enq0sym  7430  enq0ref  7431  enq0tr  7432  nqnq0pi  7436  nq0nn  7440  addnq0mo  7445  mulnq0mo  7446  nqpnq0nq  7451  nqnq0a  7452  nqnq0m  7453  npsspw  7469  elnp1st2nd  7474  prnmaxl  7486  prnminu  7487  prarloc  7501  genprndl  7519  genprndu  7520  nqprm  7540  nqprl  7549  nqpru  7550  addnqprlemrl  7555  addnqprlemru  7556  prmuloc  7564  mulnqprlemrl  7571  mulnqprlemru  7572  ltsopr  7594  ltexprlemm  7598  ltexprlemopl  7599  ltexprlemopu  7601  lteupri  7615  recexprlemopl  7623  recexprlemopu  7625  recexprlemdisj  7628  archpr  7641  cauappcvgprlemdisj  7649  cauappcvgprlemladdrl  7655  cauappcvgprlem2  7658  caucvgprlemnbj  7665  caucvgprlemdisj  7672  caucvgprlemladdfu  7675  caucvgprlem2  7678  caucvgprprlemnbj  7691  caucvgprprlemdisj  7700  suplocexprlemml  7714  suplocexprlemrl  7715  suplocexprlemmu  7716  suplocexprlemloc  7719  addsrmo  7741  mulsrmo  7742  recexgt0sr  7771  prsrpos  7783  caucvgsrlemasr  7788  suplocsrlemb  7804  suplocsrlempr  7805  suplocsr  7807  elrealeu  7827  pitonn  7846  pitoregt0  7847  pitore  7848  recnnre  7849  axaddcl  7862  axaddrcl  7863  axmulcl  7864  axmulrcl  7865  axrnegex  7877  axcnre  7879  axpre-lttrn  7882  rereceu  7887  axarch  7889  axpre-suploclemres  7899  axpre-suploc  7900  ltxrlt  8022  apirr  8561  divmulasscomap  8652  rerecclap  8686  lbreu  8901  arch  9172  0mnnnnn0  9207  nnm1nn0  9216  elnnnn0c  9220  elnnz1  9275  ztri3or0  9294  nzadd  9304  nn0n0n1ge2  9322  zdceq  9327  zdcle  9328  zdclt  9329  uzind  9363  eluzge3nn  9571  supinfneg  9594  infsupneg  9595  eluz2b2  9602  elnn1uz2  9606  elnn0dc  9610  elnndc  9611  nn01to3  9616  znq  9623  qaddcl  9634  qmulcl  9636  qreccl  9641  irradd  9645  irrmul  9646  elpq  9647  cnref1o  9649  xnn0dcle  9801  xrpnfdc  9841  xrmnfdc  9842  xaddcom  9860  xnegdi  9867  xpncan  9870  xleadd1a  9872  iooidg  9908  elioo4g  9933  elfzd  10015  fzdcel  10039  fznlem  10040  fzpreddisj  10070  fz0to4untppr  10123  elfz0ubfz0  10124  elfz0fzfz0  10125  fz0fzelfz0  10126  fz0fzdiffz0  10129  elfzmlbp  10131  difelfzle  10133  4fvwrd4  10139  fzosplit  10176  elfzo0  10181  fzo1fzo0n0  10182  elfzonn0  10185  fzofzim  10187  elfzo1  10189  elfzom1elp1fzo  10201  fzossfzop1  10211  ssfzo12bi  10224  exfzdc  10239  qdceq  10246  exbtwnzlemstep  10247  exbtwnzlemex  10249  exbtwnz  10250  rebtwn2zlemstep  10252  rebtwn2z  10254  qbtwnxr  10257  modfzo0difsn  10394  frec2uzrand  10404  frec2uzf1od  10405  frecuzrdgrcl  10409  frecuzrdgtcl  10411  frecuzrdgrclt  10414  frecuzrdgfunlem  10418  frecfzennn  10425  seq3f1olemp  10501  seq3f1oleml  10502  ser0f  10514  expcl2lemap  10531  hashunsng  10786  shftfvalg  10826  shftfval  10829  caucvgre  10989  rexanuz  10996  recvguniq  11003  rennim  11010  resqrexlemf  11015  rsqrmo  11035  fimaxre2  11234  climeu  11303  sumdc  11365  summodc  11390  zsumdc  11391  isum  11392  fisumss  11399  isumss2  11400  fsumsplit  11414  sumsnf  11416  fsumsplitsn  11417  sumtp  11421  sumsplitdc  11439  fsum2dlemstep  11441  fisum0diag2  11454  fsumconst  11461  modfsummodlemstep  11464  fsum00  11469  fsumabs  11472  fsumiun  11484  isumlessdc  11503  expcnv  11511  prodmodc  11585  zproddc  11586  iprodap  11587  iprodap0  11589  fprodssdc  11597  prodsnf  11599  fprodsplitdc  11603  fprodsplit  11604  fprodm1  11605  fprod1p  11606  fprodunsn  11611  fprod2dlemstep  11629  fprodsplitsn  11640  ef0lem  11667  modmulconst  11829  dvdsdivcl  11855  dvdsssfz1  11857  dvdsfac  11865  zeoxor  11873  nn0ehalf  11907  nn0oddm1d2  11913  nnoddm1d2  11914  divalglemeunn  11925  divalglemeuneg  11927  zsupcllemstep  11945  infssuzex  11949  gcdsupex  11957  gcdsupcl  11958  bezoutlemnewy  11996  bezoutlemmain  11998  bezoutlemeu  12007  dfgcd2  12014  nnwosdc  12039  algrf  12044  algcvgblem  12048  lcmgcdlem  12076  lcmdvds  12078  coprmgcdb  12087  mulgcddvds  12093  qredeu  12096  cncongr1  12102  cncongr2  12103  isprm2lem  12115  dvdsnprmd  12124  prmdc  12129  oddprmge3  12134  pw2dvdseu  12167  phibndlem  12215  dfphi2  12219  hashdvds  12220  phiprmpw  12221  eulerthlemh  12230  hashgcdeq  12238  phisum  12239  odzdvds  12244  reumodprminv  12252  nnnn0modprm0  12254  prm23ge5  12263  pclemdc  12287  pcdvdsb  12318  difsqpwdvds  12336  oddprmdvds  12351  1arith  12364  4sqlem3  12387  ennnfonelemdc  12399  ennnfonelemh  12404  ennnfonelemhf1o  12413  ennnfonelemf1  12418  ennnfonelemrn  12419  ennnfonelemdm  12420  exmidunben  12426  ctinfomlemom  12427  ctinfom  12428  ctiunctlemudc  12437  ctiunctlemf  12438  ctiunctal  12441  nninfdclemcl  12448  nninfdclemf  12449  nninfdclemp1  12450  isstructim  12475  setsresg  12499  strleund  12561  1strbas  12575  2strbasg  12577  2stropg  12578  restsspw  12697  tgval  12710  ptex  12712  imasaddfnlemg  12734  fnpr2o  12757  fnpr2ob  12758  mgmidsssn0  12802  isnsgrp  12811  sgrpidmndm  12820  mndinvmod  12845  mnd1  12846  mhmeql  12875  grpinveu  12910  mulgval  12985  subgintm  13056  trivsubgsnd  13059  eqgfval  13079  iscmnd  13099  srgfcl  13154  reldvdsrsrg  13259  subrgdvds  13354  istopon  13483  toponcom  13497  topgele  13499  topontopn  13507  tsettps  13508  eltg2b  13524  unitg  13532  tgss2  13549  bastop2  13554  distop  13555  epttop  13560  cldss2  13576  neisspw  13618  neipsm  13624  neiuni  13631  tgcn  13678  tgcnp  13679  cnntr  13695  lmff  13719  txuni2  13726  txbasex  13727  txbas  13728  txcnp  13741  txcnmpt  13743  txcn  13745  txdis  13747  txdis1cn  13748  cnmpt11  13753  cnmpt12  13757  cnmpt21  13761  cnmpt2t  13763  cnmpt22  13764  blsscls2  13963  xmetxpbl  13978  xmettxlem  13979  tgqioo  14017  fsumcncntop  14026  cncfmpt1f  14054  mulcncflem  14060  mulcncf  14061  dedekindeu  14071  dedekindicclemicc  14080  dedekindicc  14081  ivthinclemdisj  14088  limcimo  14104  cnmptlimc  14113  reldvg  14118  dvfvalap  14120  dvfgg  14127  dveflem  14157  dvef  14158  sincn  14160  coscn  14161  reeff1o  14164  pilem3  14174  ioocosf1o  14245  lgsne0  14409  lgseisenlem2  14421  2sqlem2  14432  mul2sq  14433  2sqlem3  14434  2sqlem7  14438  bj-trst  14461  bj-fast  14463  bj-stand  14470  bj-trdc  14474  bj-fadc  14476  decidr  14518  djulclALT  14523  djurclALT  14524  bj-charfunr  14532  bj-indind  14654  bj-2inf  14660  bj-nntrans2  14674  bj-peano4  14677  bj-nnord  14680  bj-inf2vn  14696  bj-inf2vn2  14697  bj-findis  14701  pwf1oexmid  14719  subctctexmid  14720  nnsf  14724  nninfsellemdc  14729  nninffeq  14739  exmidsbthrlem  14740  sbthom  14744  triap  14747  trilpo  14761  apdifflemr  14765  redcwlpo  14773  tridceq  14774  nconstwlpolem0  14780  nconstwlpolem  14782  nconstwlpo  14783  neapmkv  14785  ltlenmkv  14787