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  421  mpnanrd  704  oibabs  726  dcim  853  dcstab  856  stdcndc  857  stdcndcOLD  858  dcand  945  dcor  948  dfifp2dc  994  3mix1  1197  3mix2  1198  3jca  1208  syl3anbrc  1212  syl21anbrc  1213  inegd  1421  pclem6  1423  xoranor  1426  dcfrompeirce  1499  nfxfrd  1528  nfd  1576  hban  1600  nfan1  1617  nford  1620  nfand  1621  hbim1  1623  nfal  1629  alexim  1698  nnal  1702  hbn  1703  nf4r  1723  19.34  1736  nfexd  1814  sbcof2  1863  nfsb2or  1890  sbidm  1904  nfdv  1930  nfd2  2082  nfeudv  2101  mon  2115  eumo  2118  mo23  2128  eu2  2131  eu3h  2132  exmodc  2137  exmonim  2138  mo2r  2139  mo3h  2140  bm1.1  2223  eqrdv  2236  3eltr4g  2324  abbi2dv  2359  abbi1dv  2360  nfcd  2387  nfcxfrd  2390  dcned  2426  neqned  2427  3netr4g  2455  necon3bi  2470  necon2ai  2474  nnral  2540  alral  2595  rspe  2599  rsp2e  2601  rgen2a  2604  ralrimi  2621  r19.27v  2678  r19.28v  2679  r19.27av  2686  r19.32r  2697  nfreudxy  2725  mormo  2769  nrexrmo  2774  cgsex2g  2858  cgsex4g  2859  spc2egv  2915  spc2gv  2916  spc3egv  2917  spc3gv  2918  rspce  2924  ceqex  2953  elrab3t  2981  elrabd  2984  mosubt  3003  mo2icl  3005  reu3  3016  reu6i  3017  2rmorex  3032  sbc5  3075  rspesbca  3137  rmo2ilem  3142  sbnfc2  3208  ssrd  3253  ssrdv  3254  3sstr4g  3291  eqsstrid  3294  ss2abdv  3321  abssdv  3322  rabssdv  3328  ss2rabdv  3329  ssun1  3392  unssad  3406  unssbd  3407  ssddif  3465  uneqin  3482  indifdir  3487  undif3ss  3492  reuss2  3513  n0rf  3534  reximdva0m  3537  rabxmdc  3554  ssindif0im  3583  minel  3585  ralidm  3625  ralm  3628  dcun  3634  ifmdc  3680  ifeqeqxdc  3684  disjsn2  3768  rabsnif  3774  absneu  3779  rabsneu  3780  opprc  3920  elunii  3935  dfnfc2  3948  uniss2  3961  unidif  3962  ssunieq  3963  intab  3994  iunss2  4052  iunssd  4053  iunxdif2  4056  invdisj  4118  disjiun  4120  3brtr4g  4159  trin  4234  triun  4237  truni  4238  trint  4239  iinexgm  4285  class2seteq  4295  pwuni  4324  exmid1dc  4332  exmidn0m  4333  exmidsssn  4334  exmid0el  4336  exmidel  4337  exmidundif  4338  exmidundifim  4339  exmid1stab  4340  mss  4361  copsex2t  4380  euotd  4390  pwunim  4426  ispod  4444  sotricim  4463  exse  4476  frind  4492  trssord  4520  suctr  4561  pwnex  4590  eusvnf  4594  eusvnfb  4595  eusv2nf  4597  rexxfrd  4604  ralxfr2d  4605  rexxfr2d  4606  rabxfrd  4610  reuhypd  4612  eldifpw  4618  iunpw  4621  ssorduni  4629  onsucb  4645  onsucelsucr  4650  sucunielr  4652  ontriexmidim  4664  ordtri2or2exmidlem  4668  onsucelsucexmid  4672  reg2exmidlema  4676  setindel  4680  elirr  4683  orddisj  4688  en2lp  4696  suc11g  4699  ordsuc  4705  nlimsucg  4708  ordtri2or2exmid  4713  ontri2orexmidim  4714  zfregfr  4716  wessep  4720  tfi  4724  peano5  4740  limom  4756  peano2b  4757  nndceq0  4760  nnpredcl  4765  0nelrel  4816  eqrelrdv  4866  xpsspw  4882  relint  4896  relop  4925  eqbrrdva  4945  ssrelrn  4967  opeldm  4979  reldmm  4995  elres  5094  relssres  5096  elrelimasn  5148  exse2  5156  issref  5165  trin2  5174  dminss  5197  imainss  5198  rnxpid  5217  dmsn0el  5252  dmmptg  5280  relrelss  5309  cnviinm  5324  iotanul  5348  sniota  5363  dffun5r  5384  funmo  5387  funco  5412  funun  5417  fununmo  5418  fununfun  5419  funprg  5426  funtpg  5427  funtp  5429  fntpg  5432  fununi  5444  funcnvuni  5445  imadiflem  5455  imainlem  5457  funimaexglem  5459  isarep2  5463  fnunsn  5485  2elresin  5489  fnimadisj  5499  dmmptd  5509  fco  5547  funssxp  5552  fssres  5560  feu  5569  fimacnvdisj  5571  fabexg  5574  f00  5579  f0rn0  5582  f1co  5605  fores  5620  foco  5621  f1ores  5649  foimacnv  5652  f1oun  5654  fun11iun  5655  f1oco  5657  fo00  5672  brprcneu  5683  fv3  5713  relelfvdm  5722  nfvres  5726  nfunsn  5727  funfvbrb  5813  respreima  5827  dff2  5843  dff3im  5844  dffo4  5847  fvmptelcdm  5852  ffvresb  5862  f1oresrab  5864  fmptco  5865  fsn  5871  fcof  5885  fpr  5888  ftpg  5890  fsnunf  5906  fsnunfv  5907  elabrex  5953  dff1o6  5972  foeqcnvco  5986  fliftel1  5990  isores1  6010  isoini2  6015  riotasbc  6045  acexmidlemph  6068  acexmidlemcase  6070  oprabidlem  6106  brabvv  6124  eloprabga  6165  fnoprabg  6179  caovimo  6273  oprabexd  6350  uchoice  6361  fo1stresm  6385  fo2ndresm  6386  unielxp  6398  1st2ndbr  6408  opabn1stprc  6419  fmpoco  6442  1stconst  6447  2ndconst  6448  poxp  6458  spc2ed  6459  disjxp1  6462  elmpom  6464  suppsnopdc  6480  reldmtpos  6514  tposfun  6521  dftpos4  6524  smores  6553  smores2  6555  tfrlem1  6569  tfr0dm  6583  tfrlemibxssdm  6588  tfrlemibex  6590  tfrlemiubacc  6591  tfrlemi14d  6594  tfrexlem  6595  tfri1d  6596  tfr1onlembxssdm  6604  tfr1onlembex  6606  tfr1onlemubacc  6607  tfr1onlemres  6610  tfrcllemsucfn  6614  tfrcllembxssdm  6617  tfrcllembex  6619  tfrcllemubacc  6620  tfrcllemres  6623  tfri3  6628  rdgon  6647  frecabcl  6660  frecfcllem  6665  frecrdg  6669  2oconcl  6702  nnsucelsuc  6754  nntri3or  6756  nndceq  6762  nndcel  6763  dcdifsnid  6767  ecexr  6802  brdifun  6824  ecelqsdm  6869  iinerm  6871  eroveu  6890  erovlem  6891  ecopovtrn  6896  ecopovtrng  6899  th3qlem1  6901  fsetdmprc0  6940  pmsspw  6954  map0b  6958  mapsnd  6960  mapsn  6962  mapsncnv  6967  ixpf  6992  uniixp  6993  ixpexgg  6994  resixp  7005  f1oen3g  7030  ssdomg  7055  domtr  7062  snfig  7093  modom  7098  enpr2d  7101  dom1o  7106  xpf1o  7134  xpmapenlem  7139  php5dom  7154  fidceq  7161  nnfi  7164  fiunsnnn  7175  findcard  7182  findcard2  7183  findcard2s  7184  ac6sfi  7192  fidcen  7193  tridc  7194  fimax2gtri  7196  finexdc  7197  elssdc  7199  eqsndc  7200  exmidpw  7205  exmidpweq  7206  exmidpw2en  7209  nnwetri  7213  unsnfi  7216  unsnfidcex  7217  unsnfidcel  7218  undifdcss  7220  tpfidisj  7226  tpfidceq  7227  exmidssfi  7236  iunfidisj  7250  mapfi  7251  fissfi  7253  snexxph  7257  fidcenumlemrks  7260  sbthlem2  7265  sbthlemi3  7266  sbthlem7  7270  sbthlemi8  7271  fival  7294  dcfi  7305  fdcf1  7306  f1setfi  7307  supmoti  7323  djuss  7400  updjudhf  7409  updjud  7412  casefun  7415  caseinj  7419  omp1eomlem  7424  djufun  7434  djuinj  7436  ctssdccl  7441  ctfoex  7448  nnnninf  7456  nnnninfeq2  7459  nninfisollem0  7460  nninfisollemne  7461  nninfisollemeq  7462  nninfisol  7463  finomni  7470  exmidomniim  7471  exmidomni  7472  fodjuomnilemdc  7474  omniwomnimkv  7497  nninfdcinf  7501  nninfwlporlem  7503  nninfwlpoimlemg  7505  nninfwlpoim  7509  nninfinfwlpo  7510  exmidonfinlem  7535  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  finacn  7550  exmidaclem  7554  dju1en  7559  exmidontriimlem1  7567  exmidontriimlem3  7569  iftrueb01  7572  pw1on  7575  3nsssucpw1  7585  2omotaplemap  7613  2omotap  7615  exmidmotap  7617  cc4f  7625  cc4n  7627  acnccim  7628  dmaddpqlem  7734  nqpi  7735  dmaddpq  7736  dmmulpq  7737  ltdcnq  7754  subhalfnqq  7771  enq0sym  7789  enq0ref  7790  enq0tr  7791  nqnq0pi  7795  nq0nn  7799  addnq0mo  7804  mulnq0mo  7805  nqpnq0nq  7810  nqnq0a  7811  nqnq0m  7812  npsspw  7828  elnp1st2nd  7833  prnmaxl  7845  prnminu  7846  prarloc  7860  genprndl  7878  genprndu  7879  nqprm  7899  nqprl  7908  nqpru  7909  addnqprlemrl  7914  addnqprlemru  7915  prmuloc  7923  mulnqprlemrl  7930  mulnqprlemru  7931  ltsopr  7953  ltexprlemm  7957  ltexprlemopl  7958  ltexprlemopu  7960  lteupri  7974  recexprlemopl  7982  recexprlemopu  7984  recexprlemdisj  7987  archpr  8000  cauappcvgprlemdisj  8008  cauappcvgprlemladdrl  8014  cauappcvgprlem2  8017  caucvgprlemnbj  8024  caucvgprlemdisj  8031  caucvgprlemladdfu  8034  caucvgprlem2  8037  caucvgprprlemnbj  8050  caucvgprprlemdisj  8059  suplocexprlemml  8073  suplocexprlemrl  8074  suplocexprlemmu  8075  suplocexprlemloc  8078  addsrmo  8100  mulsrmo  8101  recexgt0sr  8130  prsrpos  8142  caucvgsrlemasr  8147  suplocsrlemb  8163  suplocsrlempr  8164  suplocsr  8166  elrealeu  8186  pitonn  8205  pitoregt0  8206  pitore  8207  recnnre  8208  axaddcl  8221  axaddrcl  8222  axmulcl  8223  axmulrcl  8224  axrnegex  8236  axcnre  8238  axpre-lttrn  8241  rereceu  8246  axarch  8248  axpre-suploclemres  8258  axpre-suploc  8259  ltxrlt  8381  apirr  8923  divmulasscomap  9016  rerecclap  9050  lbreu  9265  arch  9539  0mnnnnn0  9574  nnm1nn0  9583  elnnnn0c  9587  elnnz1  9646  ztri3or0  9665  nzadd  9676  nn0n0n1ge2  9694  zdceq  9699  zdcle  9700  zdclt  9701  uzind  9736  eluzge3nn  9951  supinfneg  9974  infsupneg  9975  eluz2b2  9982  elnn1uz2  9986  elnn0dc  9990  elnndc  9991  nn01to3  9996  znq  10003  qaddcl  10014  qmulcl  10016  qreccl  10021  irradd  10025  irrmul  10026  elpq  10028  cnref1o  10030  xnn0dcle  10183  xrpnfdc  10223  xrmnfdc  10224  xaddcom  10242  xnegdi  10249  xpncan  10252  xleadd1a  10254  iooidg  10290  elioo4g  10315  elfzd  10398  fzdcel  10423  fznlem  10424  fzpreddisj  10456  fz0to4untppr  10509  elfz0ubfz0  10510  elfz0fzfz0  10511  fz0fzelfz0  10512  fz0fzdiffz0  10515  elfzmlbp  10517  difelfzle  10519  4fvwrd4  10525  fzosplit  10564  elfzo0  10571  nn0p1elfzo  10572  fzo1fzo0n0  10573  elfzonn0  10576  fzofzim  10578  elfzo1  10581  elfzom1elp1fzo  10598  fzossfzop1  10608  ssfzo12bi  10621  exfzdc  10637  zsupcllemstep  10640  infssuzex  10644  qdceq  10657  qdclt  10658  exbtwnzlemstep  10660  exbtwnzlemex  10662  exbtwnz  10663  rebtwn2zlemstep  10665  rebtwn2z  10667  qbtwnxr  10670  modfzo0difsn  10810  frec2uzrand  10820  frec2uzf1od  10821  frecuzrdgrcl  10825  frecuzrdgtcl  10827  frecuzrdgrclt  10830  frecuzrdgfunlem  10834  frecfzennn  10841  nninfinf  10858  seq3f1olemp  10930  seq3f1oleml  10931  seqf1oglem1  10934  ser0f  10949  expcl2lemap  10966  hashunsng  11226  hashmap  11246  sshashneg  11259  hashfibclem  11260  hashfibc  11261  hashf1lem1  11263  hashf1lem2  11264  iswrdinn0  11287  snopiswrd  11292  wrdlndm  11299  iswrdsymb  11300  wrdsymb1  11319  ccatfv0  11349  ccatval21sw  11351  lswccatn0lsw  11357  eqs1  11374  ccat1st1st  11387  lswccats1fst  11390  fzowrddc  11397  swrdfv0  11404  swrdlen2  11412  swrdfv2  11413  swrdsbslen  11416  swrdspsleq  11417  pfxfv0  11442  pfxtrcfv0  11444  pfxeq  11446  pfx1  11453  swrdswrdlem  11454  cats1un  11471  pfxccatin12lem2a  11477  pfxccatin12lem2  11481  pfxccatin12lem3  11482  swrdccat  11485  cats1fvn  11514  cats1fvnd  11515  shftfvalg  11561  shftfval  11564  caucvgre  11725  rexanuz  11732  recvguniq  11739  rennim  11746  resqrexlemf  11751  rsqrmo  11771  fimaxre2  11971  climeu  12040  sumdc  12102  summodc  12128  zsumdc  12129  isum  12130  fisumss  12137  isumss2  12138  fsumsplit  12152  sumsnf  12154  fsumsplitsn  12155  sumtp  12159  sumsplitdc  12177  fsum2dlemstep  12179  fisum0diag2  12192  fsumconst  12199  modfsummodlemstep  12202  fsum00  12207  fsumabs  12210  fsumiun  12222  isumlessdc  12241  expcnv  12249  prodmodc  12323  zproddc  12324  iprodap  12325  iprodap0  12327  fprodssdc  12335  prodsnf  12337  fprodsplitdc  12341  fprodsplit  12342  fprodm1  12343  fprod1p  12344  fprodunsn  12349  fprod2dlemstep  12367  fprodsplitsn  12378  ef0lem  12405  modmulconst  12568  dvdsdivcl  12595  dvdsssfz1  12597  dvdsfac  12605  zeoxor  12614  nn0ehalf  12648  nn0oddm1d2  12654  nnoddm1d2  12655  divalglemeunn  12666  divalglemeuneg  12668  bitsfzolem  12699  bitsinv1  12707  gcdsupex  12712  gcdsupcl  12713  bezoutlemnewy  12751  bezoutlemmain  12753  bezoutlemeu  12762  dfgcd2  12769  nnwosdc  12794  nninfct  12796  algrf  12801  algcvgblem  12805  lcmgcdlem  12833  lcmdvds  12835  coprmgcdb  12844  mulgcddvds  12850  qredeu  12853  cncongr1  12859  cncongr2  12860  isprm2lem  12872  dvdsnprmd  12881  prmdc  12886  oddprmge3  12891  pw2dvdseu  12924  phibndlem  12972  dfphi2  12976  hashdvds  12977  phiprmpw  12978  eulerthlemh  12987  hashgcdeq  12996  phisum  12997  odzdvds  13002  reumodprminv  13010  nnnn0modprm0  13012  prm23ge5  13021  pclemdc  13045  pcdvdsb  13077  difsqpwdvds  13095  oddprmdvds  13111  1arith  13124  4sqlem3  13147  4sqlemafi  13152  4sqlemffi  13153  4sqleminfi  13154  4sqexercise1  13155  4sqlem11  13158  4sqlem19  13166  ballotfilemcdc  13201  ballotfilemdifcfi  13203  ballotfilemdifcfz  13205  ballotfilem2  13206  ballotfilemiex  13222  ballotfilemscl  13225  ballotfilemth  13259  ennnfonelemdc  13268  ennnfonelemh  13273  ennnfonelemhf1o  13282  ennnfonelemf1  13287  ennnfonelemrn  13288  ennnfonelemdm  13289  exmidunben  13295  ctinfomlemom  13296  ctinfom  13297  ctiunctlemudc  13306  ctiunctlemf  13307  ctiunctal  13310  nninfdclemcl  13317  nninfdclemf  13318  nninfdclemp1  13319  isstructim  13344  setsresg  13368  strleund  13434  1strbas  13448  2strbasg  13451  2stropg  13452  restsspw  13580  tgval  13593  ptex  13595  imasaddfnlemg  13612  fnpr2o  13637  fnpr2ob  13638  mgmidsssn0  13681  fngzsum  13685  gzsumvalx  13686  isnsgrp  13698  sgrpidmndm  13710  mndinvmod  13735  mnd1  13739  mhmeql  13776  grpinveu  13820  mulgval  13902  subgintm  13978  trivsubgsnd  13981  eqgfval  14002  ecqusaddd  14018  ecqusaddcl  14019  ghmeql  14047  iscmnd  14078  imasabl  14117  gzsummhm2  14123  gsump1  14134  gsummhm2fi  14142  prdsinvlem  14173  rnglz  14219  srgfcl  14251  rhmopp  14456  opprlring  14477  subrgdvds  14516  lssuni  14672  lssintclm  14693  lspf  14698  qusmulrng  14841  mulgrhm2  14917  znf1o  14958  psrbagfi  14982  psrbagconcl  14986  psr1clfi  15002  mplsubgfilemcl  15013  istopon  15037  toponcom  15051  topgele  15053  topontopn  15061  tsettps  15062  eltg2b  15078  unitg  15086  tgss2  15103  bastop2  15108  distop  15109  epttop  15114  cldss2  15130  neisspw  15172  neipsm  15178  neiuni  15185  tgcn  15232  tgcnp  15233  cnntr  15249  lmff  15273  txuni2  15280  txbasex  15281  txbas  15282  txcnp  15295  txcnmpt  15297  txcn  15299  txdis  15301  txdis1cn  15302  cnmpt11  15307  cnmpt12  15311  cnmpt21  15315  cnmpt2t  15317  cnmpt22  15318  blsscls2  15517  xmetxpbl  15532  xmettxlem  15533  tgqioo  15579  fsumcncntop  15591  cncfmpt1f  15622  mulcncflem  15631  mulcncf  15632  dedekindeu  15647  dedekindicclemicc  15656  dedekindicc  15657  ivthinclemdisj  15664  hovercncf  15670  limcimo  15689  cnmptlimc  15698  reldvg  15703  dvfvalap  15705  dvfgg  15712  dvmptfsum  15749  dveflem  15750  dvef  15751  elply2  15759  sincn  15793  coscn  15794  reeff1o  15797  pilem3  15807  ioocosf1o  15878  mpodvdsmulf1o  16018  fsumdvdsmul  16019  perfectlem2  16028  lgsne0  16071  gausslemma2dlem1a  16091  gausslemma2dlem4  16097  lgseisenlem2  16104  lgseisenlem3  16105  lgsquadlem2  16111  2lgslem3  16134  2sqlem2  16148  mul2sq  16149  2sqlem3  16150  2sqlem7  16154  edgstruct  16219  pw0ss  16238  incistruhgr  16245  upgrex  16258  umgrnloop0  16272  upgr1een  16279  lfgrnloopen  16288  umgredg  16300  umgrnloop2  16306  uspgredgiedg  16333  uspgriedgedg  16334  usgrislfuspgrdom  16345  usgredg3  16369  uspgredg2vlem  16375  uspgredg2v  16376  ushgredgedg  16381  ushgredgedgloop  16383  uhgr0vsize0en  16390  usgr1e  16396  subusgr  16430  vtxedgfi  16444  vtxlpfi  16445  vtxdumgrfival  16453  1loopgrvd2fi  16460  p1evtxdeqfilem  16466  vdegp1aid  16469  wlkcprim  16505  wlk1walkdom  16514  uspgr2wlkeq  16520  upgr2wlkdc  16532  wlkres  16534  clwwlkccatlem  16555  clwwlknp  16572  umgr2cwwk2dif  16579  trlsegvdegfi  16622  eupth2lem3lem3fi  16625  eupth2lem3lem6fi  16626  eupth2lem3lem4fi  16628  eupth2lembfi  16632  depindlem1  16661  bj-trst  16681  bj-fast  16683  bj-stand  16690  bj-trdc  16694  bj-fadc  16696  decidr  16738  djulclALT  16743  djurclALT  16744  bj-charfunr  16750  bj-indind  16872  bj-2inf  16878  bj-nntrans2  16892  bj-peano4  16895  bj-nnord  16898  bj-inf2vn  16914  bj-inf2vn2  16915  bj-findis  16919  pwf1oexmid  16943  subctctexmid  16944  pw1dceq  16948  exmidnotnotr  16949  exmidcon  16950  exmidpeirce  16951  nnsf  16953  nninfsellemdc  16958  nninffeq  16968  nnnninfen  16969  exmidsbthrlem  16972  sbthom  16976  triap  16983  trilpo  16997  apdifflemr  17001  redcwlpo  17010  tridceq  17011  nconstwlpolem0  17018  nconstwlpolem  17020  nconstwlpo  17021  neapmkv  17023  ltlenmkv  17025