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 )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3584  minel  3586  ralidm  3628  ralm  3631  dcun  3637  ifmdc  3683  ifeqeqxdc  3687  disjsn2  3772  rabsnif  3778  absneu  3783  rabsneu  3784  opprc  3925  elunii  3940  dfnfc2  3953  uniss2  3966  unidif  3967  ssunieq  3968  intab  3999  iunss2  4057  iunssd  4058  iunxdif2  4061  invdisj  4123  disjiun  4125  3brtr4g  4164  trin  4239  triun  4242  truni  4243  trint  4244  iinexgm  4290  class2seteq  4300  pwuni  4329  exmid1dc  4337  exmidn0m  4338  exmidsssn  4339  exmid0el  4341  exmidel  4342  exmidundif  4343  exmidundifim  4344  exmid1stab  4345  mss  4366  copsex2t  4385  euotd  4395  pwunim  4431  ispod  4449  sotricim  4468  exse  4481  frind  4497  trssord  4525  suctr  4566  pwnex  4595  eusvnf  4599  eusvnfb  4600  eusv2nf  4602  rexxfrd  4609  ralxfr2d  4610  rexxfr2d  4611  rabxfrd  4615  reuhypd  4617  eldifpw  4623  iunpw  4626  ssorduni  4634  onsucb  4650  onsucelsucr  4655  sucunielr  4657  ontriexmidim  4669  ordtri2or2exmidlem  4673  onsucelsucexmid  4677  reg2exmidlema  4681  setindel  4685  elirr  4688  orddisj  4693  en2lp  4701  suc11g  4704  ordsuc  4710  nlimsucg  4713  ordtri2or2exmid  4718  ontri2orexmidim  4719  zfregfr  4721  wessep  4725  tfi  4729  peano5  4745  limom  4761  peano2b  4762  nndceq0  4765  nnpredcl  4770  0nelrel  4821  eqrelrdv  4871  xpsspw  4887  relint  4901  relop  4930  eqbrrdva  4950  ssrelrn  4972  opeldm  4984  reldmm  5000  elres  5099  relssres  5101  elrelimasn  5153  exse2  5161  issref  5170  trin2  5179  dminss  5202  imainss  5203  rnxpid  5222  dmsn0el  5257  dmmptg  5285  relrelss  5314  cnviinm  5329  iotanul  5353  sniota  5368  dffun5r  5389  funmo  5392  funco  5417  funun  5422  fununmo  5423  fununfun  5424  funprg  5431  funtpg  5432  funtp  5434  fntpg  5437  fununi  5449  funcnvuni  5450  imadiflem  5460  imainlem  5462  funimaexglem  5464  isarep2  5468  fnunsn  5490  2elresin  5494  fnimadisj  5504  dmmptd  5514  fco  5552  funssxp  5557  fssres  5565  feu  5574  fimacnvdisj  5576  fabexg  5579  f00  5584  f0rn0  5587  f1co  5610  fores  5625  foco  5626  f1ores  5654  foimacnv  5657  f1oun  5659  fun11iun  5660  f1oco  5662  fo00  5677  brprcneu  5688  fv3  5718  relelfvdm  5727  nfvres  5732  nfunsn  5733  funfvbrb  5822  respreima  5836  dff2  5852  dff3im  5853  dffo4  5856  fvmptelcdm  5861  ffvresb  5871  f1oresrab  5873  fmptco  5874  fsn  5880  fcof  5894  fpr  5897  ftpg  5899  fsnunf  5915  fsnunfv  5916  elabrex  5963  dff1o6  5982  foeqcnvco  5996  fliftel1  6000  isores1  6020  isoini2  6025  riotasbc  6055  acexmidlemph  6078  acexmidlemcase  6080  oprabidlem  6116  brabvv  6134  eloprabga  6175  fnoprabg  6189  caovimo  6283  oprabexd  6360  uchoice  6371  fo1stresm  6395  fo2ndresm  6396  unielxp  6408  1st2ndbr  6418  opabn1stprc  6429  fmpoco  6452  1stconst  6457  2ndconst  6458  poxp  6468  spc2ed  6469  disjxp1  6472  elmpom  6474  suppsnopdc  6490  reldmtpos  6524  tposfun  6531  dftpos4  6534  smores  6563  smores2  6565  tfrlem1  6579  tfr0dm  6593  tfrlemibxssdm  6598  tfrlemibex  6600  tfrlemiubacc  6601  tfrlemi14d  6604  tfrexlem  6605  tfri1d  6606  tfr1onlembxssdm  6614  tfr1onlembex  6616  tfr1onlemubacc  6617  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllembxssdm  6627  tfrcllembex  6629  tfrcllemubacc  6630  tfrcllemres  6633  tfri3  6638  rdgon  6657  frecabcl  6670  frecfcllem  6675  frecrdg  6679  2oconcl  6712  nnsucelsuc  6764  nntri3or  6766  nndceq  6772  nndcel  6773  dcdifsnid  6777  ecexr  6812  brdifun  6834  ecelqsdm  6879  iinerm  6881  eroveu  6900  erovlem  6901  ecopovtrn  6906  ecopovtrng  6909  th3qlem1  6911  fsetdmprc0  6950  pmsspw  6964  map0b  6968  mapsnd  6970  mapsn  6972  mapsncnv  6977  ixpf  7002  uniixp  7003  ixpexgg  7004  resixp  7015  f1oen3g  7040  ssdomg  7065  domtr  7072  snfig  7103  modom  7108  enpr2d  7111  dom1o  7116  xpf1o  7144  xpmapenlem  7149  php5dom  7164  fidceq  7171  nnfi  7174  fiunsnnn  7185  findcard  7192  findcard2  7193  findcard2s  7194  ac6sfi  7202  fidcen  7203  tridc  7204  fimax2gtri  7206  finexdc  7207  elssdc  7209  eqsndc  7210  exmidpw  7215  exmidpweq  7216  exmidpw2en  7219  nnwetri  7223  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  tpfidisj  7236  tpfidceq  7237  exmidssfi  7246  iunfidisj  7260  mapfi  7261  fissfi  7263  snexxph  7267  fidcenumlemrks  7270  sbthlem2  7275  sbthlemi3  7276  sbthlem7  7280  sbthlemi8  7281  fival  7304  dcfi  7315  fdcf1  7316  f1setfi  7317  supmoti  7333  djuss  7410  updjudhf  7419  updjud  7422  casefun  7425  caseinj  7429  omp1eomlem  7434  djufun  7444  djuinj  7446  ctssdccl  7451  ctfoex  7458  nnnninf  7466  nnnninfeq2  7469  nninfisollem0  7470  nninfisollemne  7471  nninfisollemeq  7472  nninfisol  7473  finomni  7480  exmidomniim  7481  exmidomni  7482  fodjuomnilemdc  7484  omniwomnimkv  7507  nninfdcinf  7511  nninfwlporlem  7513  nninfwlpoimlemg  7515  nninfwlpoim  7519  nninfinfwlpo  7520  exmidonfinlem  7545  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  finacn  7560  exmidaclem  7564  dju1en  7569  exmidontriimlem1  7577  exmidontriimlem3  7579  iftrueb01  7582  pw1on  7585  3nsssucpw1  7595  2omotaplemap  7623  2omotap  7625  exmidmotap  7627  cc4f  7635  cc4n  7637  acnccim  7638  dmaddpqlem  7744  nqpi  7745  dmaddpq  7746  dmmulpq  7747  ltdcnq  7764  subhalfnqq  7781  enq0sym  7799  enq0ref  7800  enq0tr  7801  nqnq0pi  7805  nq0nn  7809  addnq0mo  7814  mulnq0mo  7815  nqpnq0nq  7820  nqnq0a  7821  nqnq0m  7822  npsspw  7838  elnp1st2nd  7843  prnmaxl  7855  prnminu  7856  prarloc  7870  genprndl  7888  genprndu  7889  nqprm  7909  nqprl  7918  nqpru  7919  addnqprlemrl  7924  addnqprlemru  7925  prmuloc  7933  mulnqprlemrl  7940  mulnqprlemru  7941  ltsopr  7963  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  lteupri  7984  recexprlemopl  7992  recexprlemopu  7994  recexprlemdisj  7997  archpr  8010  cauappcvgprlemdisj  8018  cauappcvgprlemladdrl  8024  cauappcvgprlem2  8027  caucvgprlemnbj  8034  caucvgprlemdisj  8041  caucvgprlemladdfu  8044  caucvgprlem2  8047  caucvgprprlemnbj  8060  caucvgprprlemdisj  8069  suplocexprlemml  8083  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemloc  8088  addsrmo  8110  mulsrmo  8111  recexgt0sr  8140  prsrpos  8152  caucvgsrlemasr  8157  suplocsrlemb  8173  suplocsrlempr  8174  suplocsr  8176  elrealeu  8196  pitonn  8215  pitoregt0  8216  pitore  8217  recnnre  8218  axaddcl  8231  axaddrcl  8232  axmulcl  8233  axmulrcl  8234  axrnegex  8246  axcnre  8248  axpre-lttrn  8251  rereceu  8256  axarch  8258  axpre-suploclemres  8268  axpre-suploc  8269  ltxrlt  8391  apirr  8935  divmulasscomap  9028  rerecclap  9062  lbreu  9277  indconst1  9305  arch  9564  0mnnnnn0  9599  nnm1nn0  9608  elnnnn0c  9612  elnnz1  9671  ztri3or0  9690  nzadd  9701  nn0n0n1ge2  9719  zdceq  9724  zdcle  9725  zdclt  9726  uzind  9761  eluzge3nn  9981  supinfneg  10004  infsupneg  10005  eluz2b2  10012  elnn1uz2  10016  elnn0dc  10020  elnndc  10021  nn01to3  10026  znq  10033  qaddcl  10044  qmulcl  10046  qreccl  10051  irradd  10055  irrmul  10057  elpq  10059  cnref1o  10061  xnn0dcle  10214  xrpnfdc  10254  xrmnfdc  10255  xaddcom  10273  xnegdi  10280  xpncan  10283  xleadd1a  10285  iooidg  10321  elioo4g  10346  elfzd  10429  fzdcel  10454  fznlem  10455  fzpreddisj  10488  fz0to4untppr  10541  elfz0ubfz0  10542  elfz0fzfz0  10543  fz0fzelfz0  10544  fz0fzdiffz0  10547  elfzmlbp  10549  difelfzle  10551  4fvwrd4  10557  fzosplit  10596  elfzo0  10603  nn0p1elfzo  10604  fzo1fzo0n0  10605  elfzonn0  10608  fzofzim  10610  elfzo1  10613  elfzom1elp1fzo  10630  fzossfzop1  10640  ssfzo12bi  10653  exfzdc  10669  zsupcllemstep  10672  infssuzex  10676  qdceq  10689  qdclt  10690  exbtwnzlemstep  10692  exbtwnzlemex  10694  exbtwnz  10695  rebtwn2zlemstep  10697  rebtwn2z  10699  qbtwnxr  10702  modfzo0difsn  10845  frec2uzrand  10855  frec2uzf1od  10856  frecuzrdgrcl  10860  frecuzrdgtcl  10862  frecuzrdgrclt  10865  frecuzrdgfunlem  10869  frecfzennn  10876  nninfinf  10893  seq3f1olemp  10965  seq3f1oleml  10966  seqf1oglem1  10969  ser0f  10984  expcl2lemap  11001  hashunsng  11262  hashmap  11282  sshashneg  11295  hashfibclem  11296  hashfibc  11297  hashf1lem1  11299  hashf1lem2  11300  iswrdinn0  11323  snopiswrd  11328  wrdlndm  11335  iswrdsymb  11336  wrdsymb1  11355  ccatfv0  11385  ccatval21sw  11387  lswccatn0lsw  11393  eqs1  11410  ccat1st1st  11423  lswccats1fst  11426  fzowrddc  11433  swrdfv0  11440  swrdlen2  11448  swrdfv2  11449  swrdsbslen  11452  swrdspsleq  11453  pfxfv0  11478  pfxtrcfv0  11480  pfxeq  11482  pfx1  11489  swrdswrdlem  11490  cats1un  11507  pfxccatin12lem2a  11513  pfxccatin12lem2  11517  pfxccatin12lem3  11518  swrdccat  11521  cats1fvn  11550  cats1fvnd  11551  shftfvalg  11597  shftfval  11600  caucvgre  11761  rexanuz  11768  recvguniq  11775  rennim  11782  resqrexlemf  11787  rsqrmo  11807  fimaxre2  12008  climeu  12078  sumdc  12140  summodc  12166  zsumdc  12167  isum  12168  fisumss  12175  isumss2  12176  fsumsplit  12190  sumsnf  12192  fsumsplitsn  12193  sumtp  12197  sumsplitdc  12215  fsum2dlemstep  12217  fisum0diag2  12230  fsumconst  12237  modfsummodlemstep  12240  fsum00  12245  fsumabs  12248  fsumiun  12260  isumlessdc  12279  expcnv  12287  prodmodc  12361  zproddc  12362  iprodap  12363  iprodap0  12365  fprodssdc  12373  prodsnf  12375  fprodsplitdc  12379  fprodsplit  12380  fprodm1  12381  fprod1p  12382  fprodunsn  12387  fprod2dlemstep  12405  fprodsplitsn  12416  ef0lem  12443  modmulconst  12606  dvdsdivcl  12633  dvdsssfz1  12635  dvdsfac  12643  zeoxor  12652  nn0ehalf  12686  nn0oddm1d2  12692  nnoddm1d2  12693  divalglemeunn  12704  divalglemeuneg  12706  bitsfzolem  12737  bitsinv1  12745  gcdsupex  12750  gcdsupcl  12751  bezoutlemnewy  12789  bezoutlemmain  12791  bezoutlemeu  12800  dfgcd2  12807  nnwosdc  12832  nninfct  12834  algrf  12839  algcvgblem  12843  lcmgcdlem  12871  lcmdvds  12873  coprmgcdb  12882  mulgcddvds  12888  qredeu  12891  cncongr1  12897  cncongr2  12898  isprm2lem  12910  dvdsnprmd  12919  prmdc  12924  prmdcz  12925  oddprmge3  12930  pwbdvdseu  12963  nn0sqdcq  13004  phibndlem  13014  dfphi2  13018  hashdvds  13019  phiprmpw  13020  eulerthlemh  13029  hashgcdeq  13038  phisum  13039  odzdvds  13044  reumodprminv  13052  nnnn0modprm0  13054  prm23ge5  13063  pclemdc  13087  pcdvdsb  13119  difsqpwdvds  13137  oddprmdvds  13153  1arith  13166  4sqlem3  13189  4sqlemafi  13194  4sqlemffi  13195  4sqleminfi  13196  4sqexercise1  13197  4sqlem11  13200  4sqlem19  13208  ballotfilemcdc  13272  ballotfilemdifcfi  13274  ballotfilemdifcfz  13276  ballotfilem2  13277  ballotfilemiex  13293  ballotfilemscl  13296  ballotfilemth  13330  ennnfonelemdc  13339  ennnfonelemh  13344  ennnfonelemhf1o  13353  ennnfonelemf1  13358  ennnfonelemrn  13359  ennnfonelemdm  13360  exmidunben  13366  ctinfomlemom  13367  ctinfom  13368  ctiunctlemudc  13377  ctiunctlemf  13378  ctiunctal  13381  nninfdclemcl  13388  nninfdclemf  13389  nninfdclemp1  13390  isstructim  13415  setsresg  13439  strleund  13506  1strbas  13520  2strbasg  13523  2stropg  13524  restsspw  13652  tgval  13665  ptex  13667  imasaddfnlemg  13684  fnpr2o  13709  fnpr2ob  13710  mgmidsssn0  13753  fngzsum  13757  gzsumvalx  13758  isnsgrp  13770  sgrpidmndm  13782  mndinvmod  13807  mnd1  13811  mhmeql  13848  grpinveu  13892  mulgval  13974  subgintm  14050  trivsubgsnd  14053  eqgfval  14074  ecqusaddd  14090  ecqusaddcl  14091  ghmeql  14119  iscmnd  14150  imasabl  14189  gzsummhm2  14195  gsump1  14206  gsummhm2fi  14214  prdsinvlem  14245  rnglz  14293  srgfcl  14326  rhmopp  14532  opprlring  14553  subrgdvds  14592  lssuni  14749  lssintclm  14770  lspf  14775  qusmulrng  14918  mulgrhm2  14994  znf1o  15035  aspid  15066  psrbagfi  15108  psrbagconcl  15112  psr1clfi  15128  mplsubgfilemcl  15139  istopon  15163  toponcom  15177  topgele  15179  topontopn  15187  tsettps  15188  eltg2b  15204  unitg  15212  tgss2  15229  bastop2  15234  distop  15235  epttop  15240  cldss2  15256  neisspw  15298  neipsm  15304  neiuni  15311  tgcn  15358  tgcnp  15359  cnntr  15375  lmff  15399  txuni2  15406  txbasex  15407  txbas  15408  txcnp  15421  txcnmpt  15423  txcn  15425  txdis  15427  txdis1cn  15428  cnmpt11  15433  cnmpt12  15437  cnmpt21  15441  cnmpt2t  15443  cnmpt22  15444  blsscls2  15643  xmetxpbl  15658  xmettxlem  15659  tgqioo  15705  fsumcncntop  15717  cncfmpt1f  15748  mulcncflem  15757  mulcncf  15758  dedekindeu  15773  dedekindicclemicc  15782  dedekindicc  15783  ivthinclemdisj  15790  hovercncf  15796  limcimo  15815  cnmptlimc  15824  reldvg  15829  dvfvalap  15831  dvfgg  15838  dvmptfsum  15875  dveflem  15876  dvef  15877  elply2  15885  sincn  15919  coscn  15920  reeff1o  15923  pilem3  15934  ioocosf1o  16005  ppiqfi  16158  prmdvdsfi  16159  ppiprm  16170  ppinprm  16171  ppidif  16175  mpodvdsmulf1o  16185  fsumdvdsmul  16186  ppiqub  16194  perfectlem2  16198  bcmono  16202  lgsne0  16255  gausslemma2dlem1a  16275  gausslemma2dlem4  16281  lgseisenlem2  16288  lgseisenlem3  16289  lgsquadlem2  16295  2lgslem3  16318  2sqlem2  16332  mul2sq  16333  2sqlem3  16334  2sqlem7  16338  edgstruct  16403  pw0ss  16422  incistruhgr  16429  upgrex  16442  umgrnloop0  16456  upgr1een  16463  lfgrnloopen  16472  umgredg  16484  umgrnloop2  16490  uspgredgiedg  16517  uspgriedgedg  16518  usgrislfuspgrdom  16529  usgredg3  16553  uspgredg2vlem  16559  uspgredg2v  16560  ushgredgedg  16565  ushgredgedgloop  16567  uhgr0vsize0en  16574  usgr1e  16580  subusgr  16614  vtxedgfi  16628  vtxlpfi  16629  vtxdumgrfival  16637  1loopgrvd2fi  16644  p1evtxdeqfilem  16650  vdegp1aid  16653  wlkcprim  16689  wlk1walkdom  16698  uspgr2wlkeq  16704  upgr2wlkdc  16716  wlkres  16718  clwwlkccatlem  16739  clwwlknp  16756  umgr2cwwk2dif  16763  trlsegvdegfi  16806  eupth2lem3lem3fi  16809  eupth2lem3lem6fi  16810  eupth2lem3lem4fi  16812  eupth2lembfi  16816  depindlem1  16845  bj-trst  16865  bj-fast  16867  bj-stand  16874  bj-trdc  16878  bj-fadc  16880  decidr  16922  djulclALT  16927  djurclALT  16928  bj-charfunr  16934  bj-indind  17056  bj-2inf  17062  bj-nntrans2  17076  bj-peano4  17079  bj-nnord  17082  bj-inf2vn  17098  bj-inf2vn2  17099  bj-findis  17103  pwf1oexmid  17127  subctctexmid  17128  pw1dceq  17133  exmidnotnotr  17134  exmidcon  17135  exmidpeirce  17136  wexmiddc  17140  wexmiddiffi  17142  wexmiddifxylem  17143  wexmiddifxy  17144  nnsf  17146  nninfsellemdc  17151  nninffeq  17161  nnnninfen  17162  exmidsbthrlem  17165  sbthom  17169  triap  17176  trilpo  17190  apdifflemr  17194  redcwlpo  17203  tridceq  17204  nconstwlpolem0  17211  nconstwlpolem  17213  nconstwlpo  17214  neapmkv  17216  ltlenmkv  17218