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  699  oibabs  721  dcim  848  dcstab  851  stdcndc  852  stdcndcOLD  853  dcand  940  dcor  943  dfifp2dc  989  3mix1  1192  3mix2  1193  3jca  1203  syl3anbrc  1207  syl21anbrc  1208  inegd  1416  pclem6  1418  xoranor  1421  dcfrompeirce  1494  nfxfrd  1523  nfd  1571  hban  1595  nfan1  1612  nford  1615  nfand  1616  hbim1  1618  nfal  1624  alexim  1693  nnal  1697  ax6blem  1698  nf4r  1719  19.34  1732  nfexd  1809  sbcof2  1858  nfsb2or  1885  sbidm  1899  nfdv  1925  nfd2  2075  nfeudv  2094  mon  2108  eumo  2111  mo23  2121  eu2  2124  eu3h  2125  exmodc  2130  exmonim  2131  mo2r  2132  mo3h  2133  bm1.1  2216  eqrdv  2229  3eltr4g  2317  abbi2dv  2350  abbi1dv  2351  nfcd  2369  nfcxfrd  2372  dcned  2408  neqned  2409  3netr4g  2437  necon3bi  2452  necon2ai  2456  nnral  2522  alral  2577  rspe  2581  rsp2e  2583  rgen2a  2586  ralrimi  2603  r19.27v  2660  r19.28v  2661  r19.27av  2668  r19.32r  2679  nfreudxy  2707  mormo  2750  nrexrmo  2755  cgsex2g  2839  cgsex4g  2840  spc2egv  2896  spc2gv  2897  spc3egv  2898  spc3gv  2899  rspce  2905  ceqex  2933  elrab3t  2961  elrabd  2964  mosubt  2983  mo2icl  2985  reu3  2996  reu6i  2997  2rmorex  3012  sbc5  3055  rspesbca  3117  rmo2ilem  3122  sbnfc2  3188  ssrd  3232  ssrdv  3233  3sstr4g  3270  eqsstrid  3273  ss2abdv  3300  abssdv  3301  rabssdv  3307  ss2rabdv  3308  ssun1  3370  unssad  3384  unssbd  3385  ssddif  3441  uneqin  3458  indifdir  3463  undif3ss  3468  reuss2  3487  n0rf  3507  reximdva0m  3510  rabxmdc  3526  ssindif0im  3554  minel  3556  ralidm  3595  ralm  3598  dcun  3604  ifmdc  3648  disjsn2  3732  rabsnif  3738  absneu  3743  rabsneu  3744  opprc  3883  elunii  3898  dfnfc2  3911  uniss2  3924  unidif  3925  ssunieq  3926  intab  3957  iunss2  4015  iunssd  4016  iunxdif2  4019  invdisj  4081  disjiun  4083  3brtr4g  4122  trin  4197  triun  4200  truni  4201  trint  4202  iinexgm  4244  class2seteq  4253  pwuni  4282  exmid1dc  4290  exmidn0m  4291  exmidsssn  4292  exmid0el  4294  exmidel  4295  exmidundif  4296  exmidundifim  4297  exmid1stab  4298  mss  4318  copsex2t  4337  euotd  4347  pwunim  4383  ispod  4401  sotricim  4420  exse  4433  frind  4449  trssord  4477  suctr  4518  pwnex  4546  eusvnf  4550  eusvnfb  4551  eusv2nf  4553  rexxfrd  4560  ralxfr2d  4561  rexxfr2d  4562  rabxfrd  4566  reuhypd  4568  eldifpw  4574  iunpw  4577  ssorduni  4585  onsucb  4601  onsucelsucr  4606  sucunielr  4608  ontriexmidim  4620  ordtri2or2exmidlem  4624  onsucelsucexmid  4628  reg2exmidlema  4632  setindel  4636  elirr  4639  orddisj  4644  en2lp  4652  suc11g  4655  ordsuc  4661  nlimsucg  4664  ordtri2or2exmid  4669  ontri2orexmidim  4670  zfregfr  4672  wessep  4676  tfi  4680  peano5  4696  limom  4712  peano2b  4713  nndceq0  4716  nnpredcl  4721  0nelrel  4772  eqrelrdv  4822  xpsspw  4838  relint  4851  relop  4880  eqbrrdva  4900  ssrelrn  4922  opeldm  4934  reldmm  4950  elres  5049  relssres  5051  elrelimasn  5102  exse2  5110  issref  5119  trin2  5128  dminss  5151  imainss  5152  rnxpid  5171  dmsn0el  5206  dmmptg  5234  relrelss  5263  cnviinm  5278  iotanul  5302  sniota  5317  dffun5r  5338  funmo  5341  funco  5366  funun  5371  fununmo  5372  fununfun  5373  funprg  5380  funtpg  5381  funtp  5383  fntpg  5386  fununi  5398  funcnvuni  5399  imadiflem  5409  imainlem  5411  funimaexglem  5413  isarep2  5417  fnunsn  5439  2elresin  5443  fnimadisj  5453  dmmptd  5463  fco  5500  funssxp  5504  fssres  5512  feu  5519  fimacnvdisj  5521  fabexg  5524  f00  5528  f0rn0  5531  f1co  5554  fores  5569  foco  5570  f1ores  5598  foimacnv  5601  f1oun  5603  fun11iun  5604  f1oco  5606  fo00  5621  brprcneu  5632  fv3  5662  relelfvdm  5671  nfvres  5675  nfunsn  5676  funfvbrb  5760  respreima  5775  dff2  5791  dff3im  5792  dffo4  5795  fvmptelcdm  5800  ffvresb  5810  f1oresrab  5812  fmptco  5813  fsn  5819  fcof  5833  fpr  5836  ftpg  5838  fsnunf  5854  fsnunfv  5855  elabrex  5898  dff1o6  5917  foeqcnvco  5931  fliftel1  5935  isores1  5955  isoini2  5960  riotasbc  5988  acexmidlemph  6011  acexmidlemcase  6013  oprabidlem  6049  brabvv  6067  eloprabga  6108  fnoprabg  6122  caovimo  6216  oprabexd  6289  uchoice  6300  fo1stresm  6324  fo2ndresm  6325  unielxp  6337  1st2ndbr  6347  opabn1stprc  6358  fmpoco  6381  1stconst  6386  2ndconst  6387  poxp  6397  spc2ed  6398  disjxp1  6401  elmpom  6403  reldmtpos  6419  tposfun  6426  dftpos4  6429  smores  6458  smores2  6460  tfrlem1  6474  tfr0dm  6488  tfrlemibxssdm  6493  tfrlemibex  6495  tfrlemiubacc  6496  tfrlemi14d  6499  tfrexlem  6500  tfri1d  6501  tfr1onlembxssdm  6509  tfr1onlembex  6511  tfr1onlemubacc  6512  tfr1onlemres  6515  tfrcllemsucfn  6519  tfrcllembxssdm  6522  tfrcllembex  6524  tfrcllemubacc  6525  tfrcllemres  6528  tfri3  6533  rdgon  6552  frecabcl  6565  frecfcllem  6570  frecrdg  6574  2oconcl  6607  nnsucelsuc  6659  nntri3or  6661  nndceq  6667  nndcel  6668  dcdifsnid  6672  ecexr  6707  brdifun  6729  ecelqsdm  6774  iinerm  6776  eroveu  6795  erovlem  6796  ecopovtrn  6801  ecopovtrng  6804  th3qlem1  6806  pmsspw  6852  map0b  6856  mapsn  6859  mapsncnv  6864  ixpf  6889  uniixp  6890  ixpexgg  6891  resixp  6902  f1oen3g  6927  ssdomg  6952  domtr  6959  snfig  6989  modom  6994  enpr2d  6997  dom1o  7002  xpf1o  7030  xpmapenlem  7035  php5dom  7049  fidceq  7056  nnfi  7059  fiunsnnn  7070  findcard  7077  findcard2  7078  findcard2s  7079  ac6sfi  7087  fidcen  7088  tridc  7089  fimax2gtri  7091  finexdc  7092  elssdc  7094  eqsndc  7095  exmidpw  7100  exmidpweq  7101  exmidpw2en  7104  nnwetri  7108  unsnfi  7111  unsnfidcex  7112  unsnfidcel  7113  undifdcss  7115  tpfidisj  7121  tpfidceq  7122  exmidssfi  7131  iunfidisj  7145  snexxph  7149  fidcenumlemrks  7152  sbthlem2  7157  sbthlemi3  7158  sbthlem7  7162  sbthlemi8  7163  fival  7169  dcfi  7180  supmoti  7192  djuss  7269  updjudhf  7278  updjud  7281  casefun  7284  caseinj  7288  omp1eomlem  7293  djufun  7303  djuinj  7305  ctssdccl  7310  ctfoex  7317  nnnninf  7325  nnnninfeq2  7328  nninfisollem0  7329  nninfisollemne  7330  nninfisollemeq  7331  nninfisol  7332  finomni  7339  exmidomniim  7340  exmidomni  7341  fodjuomnilemdc  7343  omniwomnimkv  7366  nninfdcinf  7370  nninfwlporlem  7372  nninfwlpoimlemg  7374  nninfwlpoim  7378  nninfinfwlpo  7379  exmidonfinlem  7404  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  finacn  7419  exmidaclem  7423  dju1en  7428  exmidontriimlem1  7436  exmidontriimlem3  7438  iftrueb01  7441  pw1on  7444  3nsssucpw1  7454  2omotaplemap  7476  2omotap  7478  exmidmotap  7480  cc4f  7488  cc4n  7490  acnccim  7491  dmaddpqlem  7597  nqpi  7598  dmaddpq  7599  dmmulpq  7600  ltdcnq  7617  subhalfnqq  7634  enq0sym  7652  enq0ref  7653  enq0tr  7654  nqnq0pi  7658  nq0nn  7662  addnq0mo  7667  mulnq0mo  7668  nqpnq0nq  7673  nqnq0a  7674  nqnq0m  7675  npsspw  7691  elnp1st2nd  7696  prnmaxl  7708  prnminu  7709  prarloc  7723  genprndl  7741  genprndu  7742  nqprm  7762  nqprl  7771  nqpru  7772  addnqprlemrl  7777  addnqprlemru  7778  prmuloc  7786  mulnqprlemrl  7793  mulnqprlemru  7794  ltsopr  7816  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemopu  7823  lteupri  7837  recexprlemopl  7845  recexprlemopu  7847  recexprlemdisj  7850  archpr  7863  cauappcvgprlemdisj  7871  cauappcvgprlemladdrl  7877  cauappcvgprlem2  7880  caucvgprlemnbj  7887  caucvgprlemdisj  7894  caucvgprlemladdfu  7897  caucvgprlem2  7900  caucvgprprlemnbj  7913  caucvgprprlemdisj  7922  suplocexprlemml  7936  suplocexprlemrl  7937  suplocexprlemmu  7938  suplocexprlemloc  7941  addsrmo  7963  mulsrmo  7964  recexgt0sr  7993  prsrpos  8005  caucvgsrlemasr  8010  suplocsrlemb  8026  suplocsrlempr  8027  suplocsr  8029  elrealeu  8049  pitonn  8068  pitoregt0  8069  pitore  8070  recnnre  8071  axaddcl  8084  axaddrcl  8085  axmulcl  8086  axmulrcl  8087  axrnegex  8099  axcnre  8101  axpre-lttrn  8104  rereceu  8109  axarch  8111  axpre-suploclemres  8121  axpre-suploc  8122  ltxrlt  8245  apirr  8785  divmulasscomap  8876  rerecclap  8910  lbreu  9125  arch  9399  0mnnnnn0  9434  nnm1nn0  9443  elnnnn0c  9447  elnnz1  9502  ztri3or0  9521  nzadd  9532  nn0n0n1ge2  9550  zdceq  9555  zdcle  9556  zdclt  9557  uzind  9591  eluzge3nn  9806  supinfneg  9829  infsupneg  9830  eluz2b2  9837  elnn1uz2  9841  elnn0dc  9845  elnndc  9846  nn01to3  9851  znq  9858  qaddcl  9869  qmulcl  9871  qreccl  9876  irradd  9880  irrmul  9881  elpq  9883  cnref1o  9885  xnn0dcle  10037  xrpnfdc  10077  xrmnfdc  10078  xaddcom  10096  xnegdi  10103  xpncan  10106  xleadd1a  10108  iooidg  10144  elioo4g  10169  elfzd  10251  fzdcel  10275  fznlem  10276  fzpreddisj  10306  fz0to4untppr  10359  elfz0ubfz0  10360  elfz0fzfz0  10361  fz0fzelfz0  10362  fz0fzdiffz0  10365  elfzmlbp  10367  difelfzle  10369  4fvwrd4  10375  fzosplit  10414  elfzo0  10421  nn0p1elfzo  10422  fzo1fzo0n0  10423  elfzonn0  10426  fzofzim  10428  elfzo1  10431  elfzom1elp1fzo  10448  fzossfzop1  10458  ssfzo12bi  10471  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  qdceq  10505  qdclt  10506  exbtwnzlemstep  10508  exbtwnzlemex  10510  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2z  10515  qbtwnxr  10518  modfzo0difsn  10658  frec2uzrand  10668  frec2uzf1od  10669  frecuzrdgrcl  10673  frecuzrdgtcl  10675  frecuzrdgrclt  10678  frecuzrdgfunlem  10682  frecfzennn  10689  nninfinf  10706  seq3f1olemp  10778  seq3f1oleml  10779  seqf1oglem1  10782  ser0f  10797  expcl2lemap  10814  hashunsng  11072  iswrdinn0  11122  snopiswrd  11127  wrdlndm  11134  iswrdsymb  11135  wrdsymb1  11154  ccatfv0  11184  ccatval21sw  11186  lswccatn0lsw  11192  eqs1  11209  ccat1st1st  11222  lswccats1fst  11225  fzowrddc  11232  swrdfv0  11239  swrdlen2  11247  swrdfv2  11248  swrdsbslen  11251  swrdspsleq  11252  pfxfv0  11277  pfxtrcfv0  11279  pfxeq  11281  pfx1  11288  swrdswrdlem  11289  cats1un  11306  pfxccatin12lem2a  11312  pfxccatin12lem2  11316  pfxccatin12lem3  11317  swrdccat  11320  cats1fvn  11349  cats1fvnd  11350  shftfvalg  11396  shftfval  11399  caucvgre  11559  rexanuz  11566  recvguniq  11573  rennim  11580  resqrexlemf  11585  rsqrmo  11605  fimaxre2  11805  climeu  11874  sumdc  11936  summodc  11962  zsumdc  11963  isum  11964  fisumss  11971  isumss2  11972  fsumsplit  11986  sumsnf  11988  fsumsplitsn  11989  sumtp  11993  sumsplitdc  12011  fsum2dlemstep  12013  fisum0diag2  12026  fsumconst  12033  modfsummodlemstep  12036  fsum00  12041  fsumabs  12044  fsumiun  12056  isumlessdc  12075  expcnv  12083  prodmodc  12157  zproddc  12158  iprodap  12159  iprodap0  12161  fprodssdc  12169  prodsnf  12171  fprodsplitdc  12175  fprodsplit  12176  fprodm1  12177  fprod1p  12178  fprodunsn  12183  fprod2dlemstep  12201  fprodsplitsn  12212  ef0lem  12239  modmulconst  12402  dvdsdivcl  12429  dvdsssfz1  12431  dvdsfac  12439  zeoxor  12448  nn0ehalf  12482  nn0oddm1d2  12488  nnoddm1d2  12489  divalglemeunn  12500  divalglemeuneg  12502  bitsfzolem  12533  bitsinv1  12541  gcdsupex  12546  gcdsupcl  12547  bezoutlemnewy  12585  bezoutlemmain  12587  bezoutlemeu  12596  dfgcd2  12603  nnwosdc  12628  nninfct  12630  algrf  12635  algcvgblem  12639  lcmgcdlem  12667  lcmdvds  12669  coprmgcdb  12678  mulgcddvds  12684  qredeu  12687  cncongr1  12693  cncongr2  12694  isprm2lem  12706  dvdsnprmd  12715  prmdc  12720  oddprmge3  12725  pw2dvdseu  12758  phibndlem  12806  dfphi2  12810  hashdvds  12811  phiprmpw  12812  eulerthlemh  12821  hashgcdeq  12830  phisum  12831  odzdvds  12836  reumodprminv  12844  nnnn0modprm0  12846  prm23ge5  12855  pclemdc  12879  pcdvdsb  12911  difsqpwdvds  12929  oddprmdvds  12945  1arith  12958  4sqlem3  12981  4sqlemafi  12986  4sqlemffi  12987  4sqleminfi  12988  4sqexercise1  12989  4sqlem11  12992  4sqlem19  13000  ennnfonelemdc  13038  ennnfonelemh  13043  ennnfonelemhf1o  13052  ennnfonelemf1  13057  ennnfonelemrn  13058  ennnfonelemdm  13059  exmidunben  13065  ctinfomlemom  13066  ctinfom  13067  ctiunctlemudc  13076  ctiunctlemf  13077  ctiunctal  13080  nninfdclemcl  13087  nninfdclemf  13088  nninfdclemp1  13089  isstructim  13114  setsresg  13138  strleund  13204  1strbas  13218  2strbasg  13221  2stropg  13222  restsspw  13350  tgval  13363  ptex  13365  imasaddfnlemg  13415  fnpr2o  13440  fnpr2ob  13441  mgmidsssn0  13485  fngsum  13489  igsumvalx  13490  isnsgrp  13507  sgrpidmndm  13521  mndinvmod  13546  mnd1  13556  mhmeql  13593  grpinveu  13639  prdsinvlem  13709  mulgval  13727  subgintm  13803  trivsubgsnd  13806  eqgfval  13827  ecqusaddd  13843  ecqusaddcl  13844  ghmeql  13872  iscmnd  13903  imasabl  13941  gsumfzmhm2  13949  rnglz  13977  srgfcl  14005  rhmopp  14209  subrgdvds  14268  lssuni  14396  lssintclm  14417  lspf  14422  qusmulrng  14565  mulgrhm2  14643  znf1o  14684  psrbagfi  14706  psr1clfi  14721  mplsubgfilemcl  14732  istopon  14756  toponcom  14770  topgele  14772  topontopn  14780  tsettps  14781  eltg2b  14797  unitg  14805  tgss2  14822  bastop2  14827  distop  14828  epttop  14833  cldss2  14849  neisspw  14891  neipsm  14897  neiuni  14904  tgcn  14951  tgcnp  14952  cnntr  14968  lmff  14992  txuni2  14999  txbasex  15000  txbas  15001  txcnp  15014  txcnmpt  15016  txcn  15018  txdis  15020  txdis1cn  15021  cnmpt11  15026  cnmpt12  15030  cnmpt21  15034  cnmpt2t  15036  cnmpt22  15037  blsscls2  15236  xmetxpbl  15251  xmettxlem  15252  tgqioo  15298  fsumcncntop  15310  cncfmpt1f  15341  mulcncflem  15350  mulcncf  15351  dedekindeu  15366  dedekindicclemicc  15375  dedekindicc  15376  ivthinclemdisj  15383  hovercncf  15389  limcimo  15408  cnmptlimc  15417  reldvg  15422  dvfvalap  15424  dvfgg  15431  dvmptfsum  15468  dveflem  15469  dvef  15470  elply2  15478  sincn  15512  coscn  15513  reeff1o  15516  pilem3  15526  ioocosf1o  15597  mpodvdsmulf1o  15733  fsumdvdsmul  15734  perfectlem2  15743  lgsne0  15786  gausslemma2dlem1a  15806  gausslemma2dlem4  15812  lgseisenlem2  15819  lgseisenlem3  15820  lgsquadlem2  15826  2lgslem3  15849  2sqlem2  15863  mul2sq  15864  2sqlem3  15865  2sqlem7  15869  edgstruct  15934  pw0ss  15953  incistruhgr  15960  upgrex  15973  umgrnloop0  15987  upgr1een  15994  lfgrnloopen  16003  umgredg  16015  umgrnloop2  16021  uspgredgiedg  16048  uspgriedgedg  16049  usgrislfuspgrdom  16060  usgredg3  16084  uspgredg2vlem  16090  uspgredg2v  16091  ushgredgedg  16096  ushgredgedgloop  16098  uhgr0vsize0en  16105  usgr1e  16111  subusgr  16145  vtxedgfi  16159  vtxlpfi  16160  vtxdumgrfival  16168  1loopgrvd2fi  16175  p1evtxdeqfilem  16181  vdegp1aid  16184  wlkcprim  16220  wlk1walkdom  16229  uspgr2wlkeq  16235  upgr2wlkdc  16247  wlkres  16249  clwwlkccatlem  16270  clwwlknp  16287  umgr2cwwk2dif  16294  trlsegvdegfi  16337  eupth2lem3lem3fi  16340  eupth2lem3lem6fi  16341  eupth2lem3lem4fi  16343  eupth2lembfi  16347  depindlem1  16376  bj-trst  16386  bj-fast  16388  bj-stand  16395  bj-trdc  16399  bj-fadc  16401  decidr  16443  djulclALT  16448  djurclALT  16449  bj-charfunr  16456  bj-indind  16578  bj-2inf  16584  bj-nntrans2  16598  bj-peano4  16601  bj-nnord  16604  bj-inf2vn  16620  bj-inf2vn2  16621  bj-findis  16625  pwf1oexmid  16651  subctctexmid  16652  pw1dceq  16656  nnsf  16658  nninfsellemdc  16663  nninffeq  16673  nnnninfen  16674  exmidsbthrlem  16677  sbthom  16681  triap  16684  trilpo  16698  apdifflemr  16702  redcwlpo  16711  tridceq  16712  nconstwlpolem0  16719  nconstwlpolem  16721  nconstwlpo  16722  neapmkv  16724  ltlenmkv  16726  gfsump1  16738