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  8933  divmulasscomap  9026  rerecclap  9060  lbreu  9275  indconst1  9303  arch  9560  0mnnnnn0  9595  nnm1nn0  9604  elnnnn0c  9608  elnnz1  9667  ztri3or0  9686  nzadd  9697  nn0n0n1ge2  9715  zdceq  9720  zdcle  9721  zdclt  9722  uzind  9757  eluzge3nn  9972  supinfneg  9995  infsupneg  9996  eluz2b2  10003  elnn1uz2  10007  elnn0dc  10011  elnndc  10012  nn01to3  10017  znq  10024  qaddcl  10035  qmulcl  10037  qreccl  10042  irradd  10046  irrmul  10047  elpq  10049  cnref1o  10051  xnn0dcle  10204  xrpnfdc  10244  xrmnfdc  10245  xaddcom  10263  xnegdi  10270  xpncan  10273  xleadd1a  10275  iooidg  10311  elioo4g  10336  elfzd  10419  fzdcel  10444  fznlem  10445  fzpreddisj  10478  fz0to4untppr  10531  elfz0ubfz0  10532  elfz0fzfz0  10533  fz0fzelfz0  10534  fz0fzdiffz0  10537  elfzmlbp  10539  difelfzle  10541  4fvwrd4  10547  fzosplit  10586  elfzo0  10593  nn0p1elfzo  10594  fzo1fzo0n0  10595  elfzonn0  10598  fzofzim  10600  elfzo1  10603  elfzom1elp1fzo  10620  fzossfzop1  10630  ssfzo12bi  10643  exfzdc  10659  zsupcllemstep  10662  infssuzex  10666  qdceq  10679  qdclt  10680  exbtwnzlemstep  10682  exbtwnzlemex  10684  exbtwnz  10685  rebtwn2zlemstep  10687  rebtwn2z  10689  qbtwnxr  10692  modfzo0difsn  10832  frec2uzrand  10842  frec2uzf1od  10843  frecuzrdgrcl  10847  frecuzrdgtcl  10849  frecuzrdgrclt  10852  frecuzrdgfunlem  10856  frecfzennn  10863  nninfinf  10880  seq3f1olemp  10952  seq3f1oleml  10953  seqf1oglem1  10956  ser0f  10971  expcl2lemap  10988  hashunsng  11248  hashmap  11268  sshashneg  11281  hashfibclem  11282  hashfibc  11283  hashf1lem1  11285  hashf1lem2  11286  iswrdinn0  11309  snopiswrd  11314  wrdlndm  11321  iswrdsymb  11322  wrdsymb1  11341  ccatfv0  11371  ccatval21sw  11373  lswccatn0lsw  11379  eqs1  11396  ccat1st1st  11409  lswccats1fst  11412  fzowrddc  11419  swrdfv0  11426  swrdlen2  11434  swrdfv2  11435  swrdsbslen  11438  swrdspsleq  11439  pfxfv0  11464  pfxtrcfv0  11466  pfxeq  11468  pfx1  11475  swrdswrdlem  11476  cats1un  11493  pfxccatin12lem2a  11499  pfxccatin12lem2  11503  pfxccatin12lem3  11504  swrdccat  11507  cats1fvn  11536  cats1fvnd  11537  shftfvalg  11583  shftfval  11586  caucvgre  11747  rexanuz  11754  recvguniq  11761  rennim  11768  resqrexlemf  11773  rsqrmo  11793  fimaxre2  11993  climeu  12062  sumdc  12124  summodc  12150  zsumdc  12151  isum  12152  fisumss  12159  isumss2  12160  fsumsplit  12174  sumsnf  12176  fsumsplitsn  12177  sumtp  12181  sumsplitdc  12199  fsum2dlemstep  12201  fisum0diag2  12214  fsumconst  12221  modfsummodlemstep  12224  fsum00  12229  fsumabs  12232  fsumiun  12244  isumlessdc  12263  expcnv  12271  prodmodc  12345  zproddc  12346  iprodap  12347  iprodap0  12349  fprodssdc  12357  prodsnf  12359  fprodsplitdc  12363  fprodsplit  12364  fprodm1  12365  fprod1p  12366  fprodunsn  12371  fprod2dlemstep  12389  fprodsplitsn  12400  ef0lem  12427  modmulconst  12590  dvdsdivcl  12617  dvdsssfz1  12619  dvdsfac  12627  zeoxor  12636  nn0ehalf  12670  nn0oddm1d2  12676  nnoddm1d2  12677  divalglemeunn  12688  divalglemeuneg  12690  bitsfzolem  12721  bitsinv1  12729  gcdsupex  12734  gcdsupcl  12735  bezoutlemnewy  12773  bezoutlemmain  12775  bezoutlemeu  12784  dfgcd2  12791  nnwosdc  12816  nninfct  12818  algrf  12823  algcvgblem  12827  lcmgcdlem  12855  lcmdvds  12857  coprmgcdb  12866  mulgcddvds  12872  qredeu  12875  cncongr1  12881  cncongr2  12882  isprm2lem  12894  dvdsnprmd  12903  prmdc  12908  oddprmge3  12913  pw2dvdseu  12946  phibndlem  12994  dfphi2  12998  hashdvds  12999  phiprmpw  13000  eulerthlemh  13009  hashgcdeq  13018  phisum  13019  odzdvds  13024  reumodprminv  13032  nnnn0modprm0  13034  prm23ge5  13043  pclemdc  13067  pcdvdsb  13099  difsqpwdvds  13117  oddprmdvds  13133  1arith  13146  4sqlem3  13169  4sqlemafi  13174  4sqlemffi  13175  4sqleminfi  13176  4sqexercise1  13177  4sqlem11  13180  4sqlem19  13188  ballotfilemcdc  13223  ballotfilemdifcfi  13225  ballotfilemdifcfz  13227  ballotfilem2  13228  ballotfilemiex  13244  ballotfilemscl  13247  ballotfilemth  13281  ennnfonelemdc  13290  ennnfonelemh  13295  ennnfonelemhf1o  13304  ennnfonelemf1  13309  ennnfonelemrn  13310  ennnfonelemdm  13311  exmidunben  13317  ctinfomlemom  13318  ctinfom  13319  ctiunctlemudc  13328  ctiunctlemf  13329  ctiunctal  13332  nninfdclemcl  13339  nninfdclemf  13340  nninfdclemp1  13341  isstructim  13366  setsresg  13390  strleund  13457  1strbas  13471  2strbasg  13474  2stropg  13475  restsspw  13603  tgval  13616  ptex  13618  imasaddfnlemg  13635  fnpr2o  13660  fnpr2ob  13661  mgmidsssn0  13704  fngzsum  13708  gzsumvalx  13709  isnsgrp  13721  sgrpidmndm  13733  mndinvmod  13758  mnd1  13762  mhmeql  13799  grpinveu  13843  mulgval  13925  subgintm  14001  trivsubgsnd  14004  eqgfval  14025  ecqusaddd  14041  ecqusaddcl  14042  ghmeql  14070  iscmnd  14101  imasabl  14140  gzsummhm2  14146  gsump1  14157  gsummhm2fi  14165  prdsinvlem  14196  rnglz  14244  srgfcl  14277  rhmopp  14483  opprlring  14504  subrgdvds  14543  lssuni  14700  lssintclm  14721  lspf  14726  qusmulrng  14869  mulgrhm2  14945  znf1o  14986  aspid  15017  psrbagfi  15059  psrbagconcl  15063  psr1clfi  15079  mplsubgfilemcl  15090  istopon  15114  toponcom  15128  topgele  15130  topontopn  15138  tsettps  15139  eltg2b  15155  unitg  15163  tgss2  15180  bastop2  15185  distop  15186  epttop  15191  cldss2  15207  neisspw  15249  neipsm  15255  neiuni  15262  tgcn  15309  tgcnp  15310  cnntr  15326  lmff  15350  txuni2  15357  txbasex  15358  txbas  15359  txcnp  15372  txcnmpt  15374  txcn  15376  txdis  15378  txdis1cn  15379  cnmpt11  15384  cnmpt12  15388  cnmpt21  15392  cnmpt2t  15394  cnmpt22  15395  blsscls2  15594  xmetxpbl  15609  xmettxlem  15610  tgqioo  15656  fsumcncntop  15668  cncfmpt1f  15699  mulcncflem  15708  mulcncf  15709  dedekindeu  15724  dedekindicclemicc  15733  dedekindicc  15734  ivthinclemdisj  15741  hovercncf  15747  limcimo  15766  cnmptlimc  15775  reldvg  15780  dvfvalap  15782  dvfgg  15789  dvmptfsum  15826  dveflem  15827  dvef  15828  elply2  15836  sincn  15870  coscn  15871  reeff1o  15874  pilem3  15884  ioocosf1o  15955  mpodvdsmulf1o  16104  fsumdvdsmul  16105  perfectlem2  16114  lgsne0  16157  gausslemma2dlem1a  16177  gausslemma2dlem4  16183  lgseisenlem2  16190  lgseisenlem3  16191  lgsquadlem2  16197  2lgslem3  16220  2sqlem2  16234  mul2sq  16235  2sqlem3  16236  2sqlem7  16240  edgstruct  16305  pw0ss  16324  incistruhgr  16331  upgrex  16344  umgrnloop0  16358  upgr1een  16365  lfgrnloopen  16374  umgredg  16386  umgrnloop2  16392  uspgredgiedg  16419  uspgriedgedg  16420  usgrislfuspgrdom  16431  usgredg3  16455  uspgredg2vlem  16461  uspgredg2v  16462  ushgredgedg  16467  ushgredgedgloop  16469  uhgr0vsize0en  16476  usgr1e  16482  subusgr  16516  vtxedgfi  16530  vtxlpfi  16531  vtxdumgrfival  16539  1loopgrvd2fi  16546  p1evtxdeqfilem  16552  vdegp1aid  16555  wlkcprim  16591  wlk1walkdom  16600  uspgr2wlkeq  16606  upgr2wlkdc  16618  wlkres  16620  clwwlkccatlem  16641  clwwlknp  16658  umgr2cwwk2dif  16665  trlsegvdegfi  16708  eupth2lem3lem3fi  16711  eupth2lem3lem6fi  16712  eupth2lem3lem4fi  16714  eupth2lembfi  16718  depindlem1  16747  bj-trst  16767  bj-fast  16769  bj-stand  16776  bj-trdc  16780  bj-fadc  16782  decidr  16824  djulclALT  16829  djurclALT  16830  bj-charfunr  16836  bj-indind  16958  bj-2inf  16964  bj-nntrans2  16978  bj-peano4  16981  bj-nnord  16984  bj-inf2vn  17000  bj-inf2vn2  17001  bj-findis  17005  pwf1oexmid  17029  subctctexmid  17030  pw1dceq  17035  exmidnotnotr  17036  exmidcon  17037  exmidpeirce  17038  wexmiddc  17042  wexmiddiffi  17044  wexmiddifxylem  17045  wexmiddifxy  17046  nnsf  17048  nninfsellemdc  17053  nninffeq  17063  nnnninfen  17064  exmidsbthrlem  17067  sbthom  17071  triap  17078  trilpo  17092  apdifflemr  17096  redcwlpo  17105  tridceq  17106  nconstwlpolem0  17113  nconstwlpolem  17115  nconstwlpo  17116  neapmkv  17118  ltlenmkv  17120