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  700  oibabs  722  dcim  849  dcstab  852  stdcndc  853  stdcndcOLD  854  dcand  941  dcor  944  dfifp2dc  990  3mix1  1193  3mix2  1194  3jca  1204  syl3anbrc  1208  syl21anbrc  1209  inegd  1417  pclem6  1419  xoranor  1422  dcfrompeirce  1495  nfxfrd  1524  nfd  1572  hban  1596  nfan1  1613  nford  1616  nfand  1617  hbim1  1619  nfal  1625  alexim  1694  nnal  1698  hbn  1699  nf4r  1719  19.34  1732  nfexd  1810  sbcof2  1859  nfsb2or  1886  sbidm  1900  nfdv  1926  nfd2  2078  nfeudv  2097  mon  2111  eumo  2114  mo23  2124  eu2  2127  eu3h  2128  exmodc  2133  exmonim  2134  mo2r  2135  mo3h  2136  bm1.1  2219  eqrdv  2232  3eltr4g  2320  abbi2dv  2355  abbi1dv  2356  nfcd  2381  nfcxfrd  2384  dcned  2420  neqned  2421  3netr4g  2449  necon3bi  2464  necon2ai  2468  nnral  2534  alral  2589  rspe  2593  rsp2e  2595  rgen2a  2598  ralrimi  2615  r19.27v  2672  r19.28v  2673  r19.27av  2680  r19.32r  2691  nfreudxy  2719  mormo  2763  nrexrmo  2768  cgsex2g  2852  cgsex4g  2853  spc2egv  2909  spc2gv  2910  spc3egv  2911  spc3gv  2912  rspce  2918  ceqex  2947  elrab3t  2975  elrabd  2978  mosubt  2997  mo2icl  2999  reu3  3010  reu6i  3011  2rmorex  3026  sbc5  3069  rspesbca  3131  rmo2ilem  3136  sbnfc2  3202  ssrd  3247  ssrdv  3248  3sstr4g  3285  eqsstrid  3288  ss2abdv  3315  abssdv  3316  rabssdv  3322  ss2rabdv  3323  ssun1  3386  unssad  3400  unssbd  3401  ssddif  3459  uneqin  3476  indifdir  3481  undif3ss  3486  reuss2  3505  n0rf  3525  reximdva0m  3528  rabxmdc  3544  ssindif0im  3572  minel  3574  ralidm  3614  ralm  3617  dcun  3623  ifmdc  3669  ifeqeqxdc  3673  disjsn2  3757  rabsnif  3763  absneu  3768  rabsneu  3769  opprc  3909  elunii  3924  dfnfc2  3937  uniss2  3950  unidif  3951  ssunieq  3952  intab  3983  iunss2  4041  iunssd  4042  iunxdif2  4045  invdisj  4107  disjiun  4109  3brtr4g  4148  trin  4223  triun  4226  truni  4227  trint  4228  iinexgm  4271  class2seteq  4281  pwuni  4310  exmid1dc  4318  exmidn0m  4319  exmidsssn  4320  exmid0el  4322  exmidel  4323  exmidundif  4324  exmidundifim  4325  exmid1stab  4326  mss  4347  copsex2t  4366  euotd  4376  pwunim  4412  ispod  4430  sotricim  4449  exse  4462  frind  4478  trssord  4506  suctr  4547  pwnex  4575  eusvnf  4579  eusvnfb  4580  eusv2nf  4582  rexxfrd  4589  ralxfr2d  4590  rexxfr2d  4591  rabxfrd  4595  reuhypd  4597  eldifpw  4603  iunpw  4606  ssorduni  4614  onsucb  4630  onsucelsucr  4635  sucunielr  4637  ontriexmidim  4649  ordtri2or2exmidlem  4653  onsucelsucexmid  4657  reg2exmidlema  4661  setindel  4665  elirr  4668  orddisj  4673  en2lp  4681  suc11g  4684  ordsuc  4690  nlimsucg  4693  ordtri2or2exmid  4698  ontri2orexmidim  4699  zfregfr  4701  wessep  4705  tfi  4709  peano5  4725  limom  4741  peano2b  4742  nndceq0  4745  nnpredcl  4750  0nelrel  4801  eqrelrdv  4851  xpsspw  4867  relint  4881  relop  4910  eqbrrdva  4930  ssrelrn  4952  opeldm  4964  reldmm  4980  elres  5079  relssres  5081  elrelimasn  5133  exse2  5141  issref  5150  trin2  5159  dminss  5182  imainss  5183  rnxpid  5202  dmsn0el  5237  dmmptg  5265  relrelss  5294  cnviinm  5309  iotanul  5333  sniota  5348  dffun5r  5369  funmo  5372  funco  5397  funun  5402  fununmo  5403  fununfun  5404  funprg  5411  funtpg  5412  funtp  5414  fntpg  5417  fununi  5429  funcnvuni  5430  imadiflem  5440  imainlem  5442  funimaexglem  5444  isarep2  5448  fnunsn  5470  2elresin  5474  fnimadisj  5484  dmmptd  5494  fco  5532  funssxp  5537  fssres  5545  feu  5554  fimacnvdisj  5556  fabexg  5559  f00  5564  f0rn0  5567  f1co  5590  fores  5605  foco  5606  f1ores  5634  foimacnv  5637  f1oun  5639  fun11iun  5640  f1oco  5642  fo00  5657  brprcneu  5668  fv3  5698  relelfvdm  5707  nfvres  5711  nfunsn  5712  funfvbrb  5796  respreima  5810  dff2  5826  dff3im  5827  dffo4  5830  fvmptelcdm  5835  ffvresb  5845  f1oresrab  5847  fmptco  5848  fsn  5854  fcof  5868  fpr  5871  ftpg  5873  fsnunf  5889  fsnunfv  5890  elabrex  5936  dff1o6  5955  foeqcnvco  5969  fliftel1  5973  isores1  5993  isoini2  5998  riotasbc  6028  acexmidlemph  6051  acexmidlemcase  6053  oprabidlem  6089  brabvv  6107  eloprabga  6148  fnoprabg  6162  caovimo  6256  oprabexd  6333  uchoice  6344  fo1stresm  6368  fo2ndresm  6369  unielxp  6381  1st2ndbr  6391  opabn1stprc  6402  fmpoco  6425  1stconst  6430  2ndconst  6431  poxp  6441  spc2ed  6442  disjxp1  6445  elmpom  6447  suppsnopdc  6463  reldmtpos  6497  tposfun  6504  dftpos4  6507  smores  6536  smores2  6538  tfrlem1  6552  tfr0dm  6566  tfrlemibxssdm  6571  tfrlemibex  6573  tfrlemiubacc  6574  tfrlemi14d  6577  tfrexlem  6578  tfri1d  6579  tfr1onlembxssdm  6587  tfr1onlembex  6589  tfr1onlemubacc  6590  tfr1onlemres  6593  tfrcllemsucfn  6597  tfrcllembxssdm  6600  tfrcllembex  6602  tfrcllemubacc  6603  tfrcllemres  6606  tfri3  6611  rdgon  6630  frecabcl  6643  frecfcllem  6648  frecrdg  6652  2oconcl  6685  nnsucelsuc  6737  nntri3or  6739  nndceq  6745  nndcel  6746  dcdifsnid  6750  ecexr  6785  brdifun  6807  ecelqsdm  6852  iinerm  6854  eroveu  6873  erovlem  6874  ecopovtrn  6879  ecopovtrng  6882  th3qlem1  6884  pmsspw  6930  map0b  6934  mapsnd  6936  mapsn  6938  mapsncnv  6943  ixpf  6968  uniixp  6969  ixpexgg  6970  resixp  6981  f1oen3g  7006  ssdomg  7031  domtr  7038  snfig  7069  modom  7074  enpr2d  7077  dom1o  7082  xpf1o  7110  xpmapenlem  7115  php5dom  7130  fidceq  7137  nnfi  7140  fiunsnnn  7151  findcard  7158  findcard2  7159  findcard2s  7160  ac6sfi  7168  fidcen  7169  tridc  7170  fimax2gtri  7172  finexdc  7173  elssdc  7175  eqsndc  7176  exmidpw  7181  exmidpweq  7182  exmidpw2en  7185  nnwetri  7189  unsnfi  7192  unsnfidcex  7193  unsnfidcel  7194  undifdcss  7196  tpfidisj  7202  tpfidceq  7203  exmidssfi  7212  iunfidisj  7226  mapfi  7227  fissfi  7229  snexxph  7233  fidcenumlemrks  7236  sbthlem2  7241  sbthlemi3  7242  sbthlem7  7246  sbthlemi8  7247  fival  7270  dcfi  7281  supmoti  7297  djuss  7374  updjudhf  7383  updjud  7386  casefun  7389  caseinj  7393  omp1eomlem  7398  djufun  7408  djuinj  7410  ctssdccl  7415  ctfoex  7422  nnnninf  7430  nnnninfeq2  7433  nninfisollem0  7434  nninfisollemne  7435  nninfisollemeq  7436  nninfisol  7437  finomni  7444  exmidomniim  7445  exmidomni  7446  fodjuomnilemdc  7448  omniwomnimkv  7471  nninfdcinf  7475  nninfwlporlem  7477  nninfwlpoimlemg  7479  nninfwlpoim  7483  nninfinfwlpo  7484  exmidonfinlem  7509  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  finacn  7524  exmidaclem  7528  dju1en  7533  exmidontriimlem1  7541  exmidontriimlem3  7543  iftrueb01  7546  pw1on  7549  3nsssucpw1  7559  2omotaplemap  7587  2omotap  7589  exmidmotap  7591  cc4f  7599  cc4n  7601  acnccim  7602  dmaddpqlem  7708  nqpi  7709  dmaddpq  7710  dmmulpq  7711  ltdcnq  7728  subhalfnqq  7745  enq0sym  7763  enq0ref  7764  enq0tr  7765  nqnq0pi  7769  nq0nn  7773  addnq0mo  7778  mulnq0mo  7779  nqpnq0nq  7784  nqnq0a  7785  nqnq0m  7786  npsspw  7802  elnp1st2nd  7807  prnmaxl  7819  prnminu  7820  prarloc  7834  genprndl  7852  genprndu  7853  nqprm  7873  nqprl  7882  nqpru  7883  addnqprlemrl  7888  addnqprlemru  7889  prmuloc  7897  mulnqprlemrl  7904  mulnqprlemru  7905  ltsopr  7927  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemopu  7934  lteupri  7948  recexprlemopl  7956  recexprlemopu  7958  recexprlemdisj  7961  archpr  7974  cauappcvgprlemdisj  7982  cauappcvgprlemladdrl  7988  cauappcvgprlem2  7991  caucvgprlemnbj  7998  caucvgprlemdisj  8005  caucvgprlemladdfu  8008  caucvgprlem2  8011  caucvgprprlemnbj  8024  caucvgprprlemdisj  8033  suplocexprlemml  8047  suplocexprlemrl  8048  suplocexprlemmu  8049  suplocexprlemloc  8052  addsrmo  8074  mulsrmo  8075  recexgt0sr  8104  prsrpos  8116  caucvgsrlemasr  8121  suplocsrlemb  8137  suplocsrlempr  8138  suplocsr  8140  elrealeu  8160  pitonn  8179  pitoregt0  8180  pitore  8181  recnnre  8182  axaddcl  8195  axaddrcl  8196  axmulcl  8197  axmulrcl  8198  axrnegex  8210  axcnre  8212  axpre-lttrn  8215  rereceu  8220  axarch  8222  axpre-suploclemres  8232  axpre-suploc  8233  ltxrlt  8355  apirr  8896  divmulasscomap  8987  rerecclap  9021  lbreu  9236  arch  9510  0mnnnnn0  9545  nnm1nn0  9554  elnnnn0c  9558  elnnz1  9617  ztri3or0  9636  nzadd  9647  nn0n0n1ge2  9665  zdceq  9670  zdcle  9671  zdclt  9672  uzind  9707  eluzge3nn  9922  supinfneg  9945  infsupneg  9946  eluz2b2  9953  elnn1uz2  9957  elnn0dc  9961  elnndc  9962  nn01to3  9967  znq  9974  qaddcl  9985  qmulcl  9987  qreccl  9992  irradd  9996  irrmul  9997  elpq  9999  cnref1o  10001  xnn0dcle  10154  xrpnfdc  10194  xrmnfdc  10195  xaddcom  10213  xnegdi  10220  xpncan  10223  xleadd1a  10225  iooidg  10261  elioo4g  10286  elfzd  10369  fzdcel  10394  fznlem  10395  fzpreddisj  10427  fz0to4untppr  10480  elfz0ubfz0  10481  elfz0fzfz0  10482  fz0fzelfz0  10483  fz0fzdiffz0  10486  elfzmlbp  10488  difelfzle  10490  4fvwrd4  10496  fzosplit  10535  elfzo0  10542  nn0p1elfzo  10543  fzo1fzo0n0  10544  elfzonn0  10547  fzofzim  10549  elfzo1  10552  elfzom1elp1fzo  10569  fzossfzop1  10579  ssfzo12bi  10592  exfzdc  10608  zsupcllemstep  10611  infssuzex  10615  qdceq  10628  qdclt  10629  exbtwnzlemstep  10631  exbtwnzlemex  10633  exbtwnz  10634  rebtwn2zlemstep  10636  rebtwn2z  10638  qbtwnxr  10641  modfzo0difsn  10781  frec2uzrand  10791  frec2uzf1od  10792  frecuzrdgrcl  10796  frecuzrdgtcl  10798  frecuzrdgrclt  10801  frecuzrdgfunlem  10805  frecfzennn  10812  nninfinf  10829  seq3f1olemp  10901  seq3f1oleml  10902  seqf1oglem1  10905  ser0f  10920  expcl2lemap  10937  hashunsng  11197  hashmap  11217  sshashneg  11230  hashfibclem  11231  hashfibc  11232  iswrdinn0  11254  snopiswrd  11259  wrdlndm  11266  iswrdsymb  11267  wrdsymb1  11286  ccatfv0  11316  ccatval21sw  11318  lswccatn0lsw  11324  eqs1  11341  ccat1st1st  11354  lswccats1fst  11357  fzowrddc  11364  swrdfv0  11371  swrdlen2  11379  swrdfv2  11380  swrdsbslen  11383  swrdspsleq  11384  pfxfv0  11409  pfxtrcfv0  11411  pfxeq  11413  pfx1  11420  swrdswrdlem  11421  cats1un  11438  pfxccatin12lem2a  11444  pfxccatin12lem2  11448  pfxccatin12lem3  11449  swrdccat  11452  cats1fvn  11481  cats1fvnd  11482  shftfvalg  11528  shftfval  11531  caucvgre  11691  rexanuz  11698  recvguniq  11705  rennim  11712  resqrexlemf  11717  rsqrmo  11737  fimaxre2  11937  climeu  12006  sumdc  12068  summodc  12094  zsumdc  12095  isum  12096  fisumss  12103  isumss2  12104  fsumsplit  12118  sumsnf  12120  fsumsplitsn  12121  sumtp  12125  sumsplitdc  12143  fsum2dlemstep  12145  fisum0diag2  12158  fsumconst  12165  modfsummodlemstep  12168  fsum00  12173  fsumabs  12176  fsumiun  12188  isumlessdc  12207  expcnv  12215  prodmodc  12289  zproddc  12290  iprodap  12291  iprodap0  12293  fprodssdc  12301  prodsnf  12303  fprodsplitdc  12307  fprodsplit  12308  fprodm1  12309  fprod1p  12310  fprodunsn  12315  fprod2dlemstep  12333  fprodsplitsn  12344  ef0lem  12371  modmulconst  12534  dvdsdivcl  12561  dvdsssfz1  12563  dvdsfac  12571  zeoxor  12580  nn0ehalf  12614  nn0oddm1d2  12620  nnoddm1d2  12621  divalglemeunn  12632  divalglemeuneg  12634  bitsfzolem  12665  bitsinv1  12673  gcdsupex  12678  gcdsupcl  12679  bezoutlemnewy  12717  bezoutlemmain  12719  bezoutlemeu  12728  dfgcd2  12735  nnwosdc  12760  nninfct  12762  algrf  12767  algcvgblem  12771  lcmgcdlem  12799  lcmdvds  12801  coprmgcdb  12810  mulgcddvds  12816  qredeu  12819  cncongr1  12825  cncongr2  12826  isprm2lem  12838  dvdsnprmd  12847  prmdc  12852  oddprmge3  12857  pw2dvdseu  12890  phibndlem  12938  dfphi2  12942  hashdvds  12943  phiprmpw  12944  eulerthlemh  12953  hashgcdeq  12962  phisum  12963  odzdvds  12968  reumodprminv  12976  nnnn0modprm0  12978  prm23ge5  12987  pclemdc  13011  pcdvdsb  13043  difsqpwdvds  13061  oddprmdvds  13077  1arith  13090  4sqlem3  13113  4sqlemafi  13118  4sqlemffi  13119  4sqleminfi  13120  4sqexercise1  13121  4sqlem11  13124  4sqlem19  13132  ballotfilemcdc  13167  ballotfilemdifcfi  13169  ballotfilemdifcfz  13171  ballotfilem2  13172  ballotfilemiex  13188  ballotfilemscl  13191  ballotfilemth  13225  ennnfonelemdc  13234  ennnfonelemh  13239  ennnfonelemhf1o  13248  ennnfonelemf1  13253  ennnfonelemrn  13254  ennnfonelemdm  13255  exmidunben  13261  ctinfomlemom  13262  ctinfom  13263  ctiunctlemudc  13272  ctiunctlemf  13273  ctiunctal  13276  nninfdclemcl  13283  nninfdclemf  13284  nninfdclemp1  13285  isstructim  13310  setsresg  13334  strleund  13400  1strbas  13414  2strbasg  13417  2stropg  13418  restsspw  13546  tgval  13559  ptex  13561  imasaddfnlemg  13578  fnpr2o  13603  fnpr2ob  13604  mgmidsssn0  13647  fngsum  13651  igsumvalx  13652  isnsgrp  13669  sgrpidmndm  13681  mndinvmod  13706  mnd1  13710  mhmeql  13747  grpinveu  13793  mulgval  13875  subgintm  13951  trivsubgsnd  13954  eqgfval  13975  ecqusaddd  13991  ecqusaddcl  13992  ghmeql  14020  iscmnd  14051  imasabl  14089  gsumfzmhm2  14097  gfsump1  14108  prdsinvlem  14138  rnglz  14184  srgfcl  14216  rhmopp  14421  opprlring  14442  subrgdvds  14481  lssuni  14637  lssintclm  14658  lspf  14663  qusmulrng  14806  mulgrhm2  14884  znf1o  14925  psrbagfi  14949  psrbagconcl  14953  psr1clfi  14969  mplsubgfilemcl  14980  istopon  15004  toponcom  15018  topgele  15020  topontopn  15028  tsettps  15029  eltg2b  15045  unitg  15053  tgss2  15070  bastop2  15075  distop  15076  epttop  15081  cldss2  15097  neisspw  15139  neipsm  15145  neiuni  15152  tgcn  15199  tgcnp  15200  cnntr  15216  lmff  15240  txuni2  15247  txbasex  15248  txbas  15249  txcnp  15262  txcnmpt  15264  txcn  15266  txdis  15268  txdis1cn  15269  cnmpt11  15274  cnmpt12  15278  cnmpt21  15282  cnmpt2t  15284  cnmpt22  15285  blsscls2  15484  xmetxpbl  15499  xmettxlem  15500  tgqioo  15546  fsumcncntop  15558  cncfmpt1f  15589  mulcncflem  15598  mulcncf  15599  dedekindeu  15614  dedekindicclemicc  15623  dedekindicc  15624  ivthinclemdisj  15631  hovercncf  15637  limcimo  15656  cnmptlimc  15665  reldvg  15670  dvfvalap  15672  dvfgg  15679  dvmptfsum  15716  dveflem  15717  dvef  15718  elply2  15726  sincn  15760  coscn  15761  reeff1o  15764  pilem3  15774  ioocosf1o  15845  mpodvdsmulf1o  15984  fsumdvdsmul  15985  perfectlem2  15994  lgsne0  16037  gausslemma2dlem1a  16057  gausslemma2dlem4  16063  lgseisenlem2  16070  lgseisenlem3  16071  lgsquadlem2  16077  2lgslem3  16100  2sqlem2  16114  mul2sq  16115  2sqlem3  16116  2sqlem7  16120  edgstruct  16185  pw0ss  16204  incistruhgr  16211  upgrex  16224  umgrnloop0  16238  upgr1een  16245  lfgrnloopen  16254  umgredg  16266  umgrnloop2  16272  uspgredgiedg  16299  uspgriedgedg  16300  usgrislfuspgrdom  16311  usgredg3  16335  uspgredg2vlem  16341  uspgredg2v  16342  ushgredgedg  16347  ushgredgedgloop  16349  uhgr0vsize0en  16356  usgr1e  16362  subusgr  16396  vtxedgfi  16410  vtxlpfi  16411  vtxdumgrfival  16419  1loopgrvd2fi  16426  p1evtxdeqfilem  16432  vdegp1aid  16435  wlkcprim  16471  wlk1walkdom  16480  uspgr2wlkeq  16486  upgr2wlkdc  16498  wlkres  16500  clwwlkccatlem  16521  clwwlknp  16538  umgr2cwwk2dif  16545  trlsegvdegfi  16588  eupth2lem3lem3fi  16591  eupth2lem3lem6fi  16592  eupth2lem3lem4fi  16594  eupth2lembfi  16598  depindlem1  16627  bj-trst  16637  bj-fast  16639  bj-stand  16646  bj-trdc  16650  bj-fadc  16652  decidr  16694  djulclALT  16699  djurclALT  16700  bj-charfunr  16706  bj-indind  16828  bj-2inf  16834  bj-nntrans2  16848  bj-peano4  16851  bj-nnord  16854  bj-inf2vn  16870  bj-inf2vn2  16871  bj-findis  16875  pwf1oexmid  16899  subctctexmid  16900  pw1dceq  16904  exmidnotnotr  16905  exmidcon  16906  exmidpeirce  16907  nnsf  16909  nninfsellemdc  16914  nninffeq  16924  nnnninfen  16925  exmidsbthrlem  16928  sbthom  16932  triap  16939  trilpo  16953  apdifflemr  16957  redcwlpo  16966  tridceq  16967  nconstwlpolem0  16975  nconstwlpolem  16977  nconstwlpo  16978  neapmkv  16980  ltlenmkv  16982