Theorem sylibr 132

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sylbbr  134  pm5.74rd  181  bitri  182  3imtr4i  199  sylanbrc  408  dcimpstab  788  dcim  820  oibabs  836  stabtestimpdc  860  dcor  879  3mix1  1110  3mix2  1111  3jca  1121  syl3anbrc  1125  inegd  1306  pclem6  1308  xoranor  1311  nfxfrd  1407  nfd  1459  hban  1482  nfan1  1499  nford  1502  nfand  1503  hbim1  1505  alexim  1579  ax6blem  1583  nf4r  1604  19.34  1617  nfexd  1688  sbcof2  1735  nfsb2or  1762  sbidm  1776  nfdv  1802  nfeudv  1960  mon  1974  eumo  1977  mo23  1986  eu2  1989  eu3h  1990  exmodc  1995  exmonim  1996  mo2r  1997  mo3h  1998  bm1.1  2070  eqrdv  2083  3eltr4g  2170  abbi2dv  2203  abbi1dv  2204  nfcd  2220  nfcxfrd  2223  dcned  2257  neqned  2258  3netr4g  2286  necon3bi  2301  necon2ai  2305  alral  2417  rspe  2420  rsp2e  2422  rgen2a  2425  ralrimi  2440  r19.27av  2500  r19.32r  2510  nfreudxy  2536  mormo  2574  nrexrmo  2579  cgsex2g  2649  cgsex4g  2650  spc2egv  2701  spc2gv  2702  spc3egv  2703  spc3gv  2704  rspce  2710  ceqex  2735  elrab3t  2761  elrabd  2764  mosubt  2783  mo2icl  2785  reu3  2796  reu6i  2797  2rmorex  2810  sbc5  2852  rspesbca  2912  rmo2ilem  2917  sbnfc2  2977  ssrd  3019  ssrdv  3020  3sstr4g  3056  syl5eqss  3059  ss2abdv  3083  abssdv  3084  rabssdv  3090  ss2rabdv  3091  ssun1  3152  unssad  3166  unssbd  3167  ssddif  3222  uneqin  3239  indifdir  3244  undif3ss  3249  reuss2  3268  n0rf  3284  reximdva0m  3287  rabxmdc  3303  ssindif0im  3330  minel  3332  ralidm  3369  ralm  3373  ifmdc  3414  disjsn2  3488  absneu  3497  rabsneu  3498  opprc  3626  elunii  3641  dfnfc2  3654  uniss2  3667  unidif  3668  ssunieq  3669  intab  3700  iunss2  3758  iunxdif2  3761  invdisj  3815  3brtr4g  3852  trin  3921  triun  3924  truni  3925  trint  3926  iinexgm  3965  class2seteq  3973  pwuni  4001  exmid0el  4007  exmidel  4008  exmidundif  4009  mss  4027  copsex2t  4046  euotd  4055  pwunim  4087  ispod  4105  sotricim  4124  exse  4137  frind  4153  trssord  4181  suctr  4222  eusvnf  4249  eusvnfb  4250  eusv2nf  4252  rexxfrd  4259  ralxfr2d  4260  rexxfr2d  4261  rabxfrd  4265  reuhypd  4267  eldifpw  4272  iunpw  4275  ssorduni  4277  sucelon  4293  onsucelsucr  4298  sucunielr  4300  ordtri2or2exmidlem  4315  onsucelsucexmid  4319  reg2exmidlema  4323  setindel  4327  elirr  4330  orddisj  4335  en2lp  4343  suc11g  4346  ordsuc  4352  nlimsucg  4355  ordtri2or2exmid  4360  zfregfr  4362  wessep  4366  tfi  4370  peano5  4386  limom  4401  peano2b  4402  nndceq0  4404  eqrelrdv  4502  xpsspw  4518  relint  4529  relop  4554  eqbrrdva  4574  opeldm  4607  elres  4715  relssres  4717  exse2  4773  issref  4781  trin2  4790  dminss  4812  imainss  4813  rnxpid  4831  dmsn0el  4866  dmmptg  4894  relrelss  4923  cnviinm  4938  iotanul  4961  sniota  4973  dffun5r  4993  funmo  4996  funco  5019  funun  5023  funprg  5029  funtpg  5030  funtp  5032  fntpg  5035  fununi  5047  funcnvuni  5048  imadiflem  5058  imainlem  5060  funimaexglem  5062  isarep2  5066  fnunsn  5086  2elresin  5090  fnimadisj  5099  fco  5140  funssxp  5144  fssres  5150  feu  5156  fimacnvdisj  5158  fabexg  5161  f00  5165  f0rn0  5168  f1co  5191  fores  5205  foco  5206  f1ores  5231  foimacnv  5234  f1oun  5236  fun11iun  5237  f1oco  5239  fo00  5252  brprcneu  5261  fv3  5291  relelfvdm  5299  nfvres  5300  nfunsn  5301  funfvbrb  5375  respreima  5390  dff2  5406  dff3im  5407  dffo4  5410  ffvresb  5424  f1oresrab  5426  fmptco  5427  fsn  5432  fpr  5442  ftpg  5444  fsnunf  5459  fsnunfv  5460  elabrex  5498  dff1o6  5516  foeqcnvco  5530  fliftel1  5534  isores1  5554  isoini2  5559  riotasbc  5584  acexmidlemph  5606  acexmidlemcase  5608  oprabidlem  5637  brabvv  5652  eloprabga  5692  fnoprabg  5703  caovimo  5795  oprabexd  5855  fo1stresm  5889  fo2ndresm  5890  unielxp  5901  1st2ndbr  5911  fmpt2co  5938  1stconst  5943  2ndconst  5944  poxp  5954  spc2ed  5955  reldmtpos  5972  tposfun  5979  dftpos4  5982  smores  6011  smores2  6013  tfrlem1  6027  tfr0dm  6041  tfrlemibxssdm  6046  tfrlemibex  6048  tfrlemiubacc  6049  tfrlemi14d  6052  tfrexlem  6053  tfri1d  6054  tfr1onlembxssdm  6062  tfr1onlembex  6064  tfr1onlemubacc  6065  tfr1onlemres  6068  tfrcllemsucfn  6072  tfrcllembxssdm  6075  tfrcllembex  6077  tfrcllemubacc  6078  tfrcllemres  6081  tfri3  6086  rdgon  6105  frecabcl  6118  frecfcllem  6123  frecrdg  6127  2oconcl  6157  nnsucelsuc  6206  nntri3or  6208  nndceq  6214  nndcel  6215  dcdifsnid  6217  ecexr  6249  brdifun  6271  ecelqsdm  6314  iinerm  6316  eroveu  6335  erovlem  6336  ecopovtrn  6341  ecopovtrng  6344  th3qlem1  6346  pmsspw  6392  map0b  6396  mapsn  6399  mapsncnv  6404  f1oen3g  6423  ssdomg  6447  domtr  6454  snfig  6483  xpf1o  6512  xpmapenlem  6517  php5dom  6531  fidceq  6537  nnfi  6540  fiunsnnn  6549  findcard  6556  findcard2  6557  findcard2s  6558  ac6sfi  6566  tridc  6567  fimax2gtri  6569  finexdc  6570  exmidpw  6576  nnwetri  6578  unsnfi  6581  unsnfidcex  6582  unsnfidcel  6583  undifdcss  6585  snexxph  6608  sbthlem2  6611  sbthlemi3  6612  sbthlem7  6616  sbthlemi8  6617  supmoti  6632  djuun  6704  djuss  6705  updjudhf  6714  updjud  6717  casefun  6720  caseinj  6724  djufun  6728  djuinj  6730  finomni  6740  exmidomniim  6741  exmidomni  6742  fodjuomnilemdc  6743  nnnninf  6750  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  dmaddpqlem  6880  nqpi  6881  dmaddpq  6882  dmmulpq  6883  ltdcnq  6900  subhalfnqq  6917  enq0sym  6935  enq0ref  6936  enq0tr  6937  nqnq0pi  6941  nq0nn  6945  addnq0mo  6950  mulnq0mo  6951  nqpnq0nq  6956  nqnq0a  6957  nqnq0m  6958  npsspw  6974  elnp1st2nd  6979  prnmaxl  6991  prnminu  6992  prarloc  7006  genprndl  7024  genprndu  7025  nqprm  7045  nqprl  7054  nqpru  7055  addnqprlemrl  7060  addnqprlemru  7061  prmuloc  7069  mulnqprlemrl  7076  mulnqprlemru  7077  ltsopr  7099  ltexprlemm  7103  ltexprlemopl  7104  ltexprlemopu  7106  lteupri  7120  recexprlemopl  7128  recexprlemopu  7130  recexprlemdisj  7133  archpr  7146  cauappcvgprlemdisj  7154  cauappcvgprlemladdrl  7160  cauappcvgprlem2  7163  caucvgprlemnbj  7170  caucvgprlemdisj  7177  caucvgprlemladdfu  7180  caucvgprlem2  7183  caucvgprprlemnbj  7196  caucvgprprlemdisj  7205  addsrmo  7233  mulsrmo  7234  recexgt0sr  7263  prsrpos  7274  caucvgsrlemasr  7279  elrealeu  7311  pitonn  7329  pitoregt0  7330  pitore  7331  recnnre  7332  axaddcl  7345  axaddrcl  7346  axmulcl  7347  axmulrcl  7348  axrnegex  7358  axcnre  7360  axpre-lttrn  7363  rereceu  7368  axarch  7370  ltxrlt  7496  apirr  8023  divmulasscomap  8102  rerecclap  8136  lbreu  8341  arch  8603  0mnnnnn0  8638  nnm1nn0  8647  elnnnn0c  8651  elnnz1  8706  ztri3or0  8725  nzadd  8735  nn0n0n1ge2  8750  zdceq  8755  zdcle  8756  zdclt  8757  uzind  8790  eluzge3nn  8992  supinfneg  9015  infsupneg  9016  eluz2b2  9022  elnn1uz2  9026  nn01to3  9034  znq  9041  qaddcl  9052  qmulcl  9054  qreccl  9059  irradd  9063  irrmul  9064  cnref1o  9065  iooidg  9259  elioo4g  9284  fzdcel  9386  fznlem  9387  fzpreddisj  9415  elfz0ubfz0  9464  elfz0fzfz0  9465  fz0fzelfz0  9466  fz0fzdiffz0  9469  elfzmlbp  9471  difelfzle  9473  4fvwrd4  9479  fzosplit  9516  elfzo0  9521  fzo1fzo0n0  9522  elfzonn0  9525  fzofzim  9527  elfzo1  9529  elfzom1elp1fzo  9541  fzossfzop1  9551  ssfzo12bi  9564  exfzdc  9579  qdceq  9586  exbtwnzlemstep  9587  exbtwnzlemex  9589  exbtwnz  9590  rebtwn2zlemstep  9592  rebtwn2z  9594  qbtwnxr  9597  modfzo0difsn  9730  frec2uzrand  9740  frec2uzf1od  9741  frecuzrdgrcl  9745  frecuzrdgtcl  9747  frecuzrdgrclt  9750  frecuzrdgfunlem  9754  frecfzennn  9761  iseqfcl  9793  iseqf1olemp  9835  iseqf1oleml  9836  iser0f  9848  expcl2lemap  9865  hashunsng  10111  shftfvalg  10148  shftfval  10151  caucvgre  10309  rexanuz  10316  recvguniq  10323  rennim  10330  resqrexlemf  10335  rsqrmo  10355  fimaxre2  10551  climeu  10577  sumdc  10637  isummo  10662  zisum  10663  iisum  10664  fisumss  10670  modmulconst  10703  dvdsdivcl  10726  dvdsssfz1  10728  dvdsfac  10736  zeoxor  10744  nn0ehalf  10778  nn0oddm1d2  10784  nnoddm1d2  10785  divalglemeunn  10796  divalglemeuneg  10798  zsupcllemstep  10816  infssuzex  10820  gcdsupex  10824  gcdsupcl  10825  bezoutlemnewy  10860  bezoutlemmain  10862  bezoutlemeu  10871  dfgcd2  10878  ialgrf  10902  algcvgblem  10906  lcmgcdlem  10934  lcmdvds  10936  coprmgcdb  10945  mulgcddvds  10951  qredeu  10954  cncongr1  10960  cncongr2  10961  isprm2lem  10973  dvdsnprmd  10982  oddprmge3  10991  pw2dvdseu  11021  phibndlem  11067  dfphi2  11071  hashdvds  11072  phiprmpw  11073  hashgcdeq  11079  bj-nfalt  11103  decidr  11134  djulclALT  11139  djurclALT  11140  bj-indind  11265  bj-2inf  11271  bj-nntrans2  11285  bj-peano4  11288  bj-nnord  11291  bj-inf2vn  11307  bj-inf2vn2  11308  bj-findis  11312  nnpredcl  11328  nnsf  11333  nninfsellemdc  11340  exmidsbthrlem  11350