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  5832  fpr  5835  ftpg  5837  fsnunf  5853  fsnunfv  5854  elabrex  5897  dff1o6  5916  foeqcnvco  5930  fliftel1  5934  isores1  5954  isoini2  5959  riotasbc  5987  acexmidlemph  6010  acexmidlemcase  6012  oprabidlem  6048  brabvv  6066  eloprabga  6107  fnoprabg  6121  caovimo  6215  oprabexd  6288  uchoice  6299  fo1stresm  6323  fo2ndresm  6324  unielxp  6336  1st2ndbr  6346  opabn1stprc  6357  fmpoco  6380  1stconst  6385  2ndconst  6386  poxp  6396  spc2ed  6397  disjxp1  6400  elmpom  6402  reldmtpos  6418  tposfun  6425  dftpos4  6428  smores  6457  smores2  6459  tfrlem1  6473  tfr0dm  6487  tfrlemibxssdm  6492  tfrlemibex  6494  tfrlemiubacc  6495  tfrlemi14d  6498  tfrexlem  6499  tfri1d  6500  tfr1onlembxssdm  6508  tfr1onlembex  6510  tfr1onlemubacc  6511  tfr1onlemres  6514  tfrcllemsucfn  6518  tfrcllembxssdm  6521  tfrcllembex  6523  tfrcllemubacc  6524  tfrcllemres  6527  tfri3  6532  rdgon  6551  frecabcl  6564  frecfcllem  6569  frecrdg  6573  2oconcl  6606  nnsucelsuc  6658  nntri3or  6660  nndceq  6666  nndcel  6667  dcdifsnid  6671  ecexr  6706  brdifun  6728  ecelqsdm  6773  iinerm  6775  eroveu  6794  erovlem  6795  ecopovtrn  6800  ecopovtrng  6803  th3qlem1  6805  pmsspw  6851  map0b  6855  mapsn  6858  mapsncnv  6863  ixpf  6888  uniixp  6889  ixpexgg  6890  resixp  6901  f1oen3g  6926  ssdomg  6951  domtr  6958  snfig  6988  modom  6993  enpr2d  6996  dom1o  7001  xpf1o  7029  xpmapenlem  7034  php5dom  7048  fidceq  7055  nnfi  7058  fiunsnnn  7069  findcard  7076  findcard2  7077  findcard2s  7078  ac6sfi  7086  fidcen  7087  tridc  7088  fimax2gtri  7090  finexdc  7091  elssdc  7093  eqsndc  7094  exmidpw  7099  exmidpweq  7100  exmidpw2en  7103  nnwetri  7107  unsnfi  7110  unsnfidcex  7111  unsnfidcel  7112  undifdcss  7114  tpfidisj  7120  tpfidceq  7121  exmidssfi  7130  iunfidisj  7144  snexxph  7148  fidcenumlemrks  7151  sbthlem2  7156  sbthlemi3  7157  sbthlem7  7161  sbthlemi8  7162  fival  7168  dcfi  7179  supmoti  7191  djuss  7268  updjudhf  7277  updjud  7280  casefun  7283  caseinj  7287  omp1eomlem  7292  djufun  7302  djuinj  7304  ctssdccl  7309  ctfoex  7316  nnnninf  7324  nnnninfeq2  7327  nninfisollem0  7328  nninfisollemne  7329  nninfisollemeq  7330  nninfisol  7331  finomni  7338  exmidomniim  7339  exmidomni  7340  fodjuomnilemdc  7342  omniwomnimkv  7365  nninfdcinf  7369  nninfwlporlem  7371  nninfwlpoimlemg  7373  nninfwlpoim  7377  nninfinfwlpo  7378  exmidonfinlem  7403  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  finacn  7418  exmidaclem  7422  dju1en  7427  exmidontriimlem1  7435  exmidontriimlem3  7437  iftrueb01  7440  pw1on  7443  3nsssucpw1  7453  2omotaplemap  7475  2omotap  7477  exmidmotap  7479  cc4f  7487  cc4n  7489  acnccim  7490  dmaddpqlem  7596  nqpi  7597  dmaddpq  7598  dmmulpq  7599  ltdcnq  7616  subhalfnqq  7633  enq0sym  7651  enq0ref  7652  enq0tr  7653  nqnq0pi  7657  nq0nn  7661  addnq0mo  7666  mulnq0mo  7667  nqpnq0nq  7672  nqnq0a  7673  nqnq0m  7674  npsspw  7690  elnp1st2nd  7695  prnmaxl  7707  prnminu  7708  prarloc  7722  genprndl  7740  genprndu  7741  nqprm  7761  nqprl  7770  nqpru  7771  addnqprlemrl  7776  addnqprlemru  7777  prmuloc  7785  mulnqprlemrl  7792  mulnqprlemru  7793  ltsopr  7815  ltexprlemm  7819  ltexprlemopl  7820  ltexprlemopu  7822  lteupri  7836  recexprlemopl  7844  recexprlemopu  7846  recexprlemdisj  7849  archpr  7862  cauappcvgprlemdisj  7870  cauappcvgprlemladdrl  7876  cauappcvgprlem2  7879  caucvgprlemnbj  7886  caucvgprlemdisj  7893  caucvgprlemladdfu  7896  caucvgprlem2  7899  caucvgprprlemnbj  7912  caucvgprprlemdisj  7921  suplocexprlemml  7935  suplocexprlemrl  7936  suplocexprlemmu  7937  suplocexprlemloc  7940  addsrmo  7962  mulsrmo  7963  recexgt0sr  7992  prsrpos  8004  caucvgsrlemasr  8009  suplocsrlemb  8025  suplocsrlempr  8026  suplocsr  8028  elrealeu  8048  pitonn  8067  pitoregt0  8068  pitore  8069  recnnre  8070  axaddcl  8083  axaddrcl  8084  axmulcl  8085  axmulrcl  8086  axrnegex  8098  axcnre  8100  axpre-lttrn  8103  rereceu  8108  axarch  8110  axpre-suploclemres  8120  axpre-suploc  8121  ltxrlt  8244  apirr  8784  divmulasscomap  8875  rerecclap  8909  lbreu  9124  arch  9398  0mnnnnn0  9433  nnm1nn0  9442  elnnnn0c  9446  elnnz1  9501  ztri3or0  9520  nzadd  9531  nn0n0n1ge2  9549  zdceq  9554  zdcle  9555  zdclt  9556  uzind  9590  eluzge3nn  9805  supinfneg  9828  infsupneg  9829  eluz2b2  9836  elnn1uz2  9840  elnn0dc  9844  elnndc  9845  nn01to3  9850  znq  9857  qaddcl  9868  qmulcl  9870  qreccl  9875  irradd  9879  irrmul  9880  elpq  9882  cnref1o  9884  xnn0dcle  10036  xrpnfdc  10076  xrmnfdc  10077  xaddcom  10095  xnegdi  10102  xpncan  10105  xleadd1a  10107  iooidg  10143  elioo4g  10168  elfzd  10250  fzdcel  10274  fznlem  10275  fzpreddisj  10305  fz0to4untppr  10358  elfz0ubfz0  10359  elfz0fzfz0  10360  fz0fzelfz0  10361  fz0fzdiffz0  10364  elfzmlbp  10366  difelfzle  10368  4fvwrd4  10374  fzosplit  10413  elfzo0  10420  fzo1fzo0n0  10421  elfzonn0  10424  fzofzim  10426  elfzo1  10429  elfzom1elp1fzo  10446  fzossfzop1  10456  ssfzo12bi  10469  exfzdc  10485  zsupcllemstep  10488  infssuzex  10492  qdceq  10503  qdclt  10504  exbtwnzlemstep  10506  exbtwnzlemex  10508  exbtwnz  10509  rebtwn2zlemstep  10511  rebtwn2z  10513  qbtwnxr  10516  modfzo0difsn  10656  frec2uzrand  10666  frec2uzf1od  10667  frecuzrdgrcl  10671  frecuzrdgtcl  10673  frecuzrdgrclt  10676  frecuzrdgfunlem  10680  frecfzennn  10687  nninfinf  10704  seq3f1olemp  10776  seq3f1oleml  10777  seqf1oglem1  10780  ser0f  10795  expcl2lemap  10812  hashunsng  11070  iswrdinn0  11117  snopiswrd  11122  wrdlndm  11129  iswrdsymb  11130  wrdsymb1  11149  ccatfv0  11179  ccatval21sw  11181  lswccatn0lsw  11187  eqs1  11204  ccat1st1st  11217  lswccats1fst  11220  fzowrddc  11227  swrdfv0  11234  swrdlen2  11242  swrdfv2  11243  swrdsbslen  11246  swrdspsleq  11247  pfxfv0  11272  pfxtrcfv0  11274  pfxeq  11276  pfx1  11283  swrdswrdlem  11284  cats1un  11301  pfxccatin12lem2a  11307  pfxccatin12lem2  11311  pfxccatin12lem3  11312  swrdccat  11315  cats1fvn  11344  cats1fvnd  11345  shftfvalg  11378  shftfval  11381  caucvgre  11541  rexanuz  11548  recvguniq  11555  rennim  11562  resqrexlemf  11567  rsqrmo  11587  fimaxre2  11787  climeu  11856  sumdc  11918  summodc  11943  zsumdc  11944  isum  11945  fisumss  11952  isumss2  11953  fsumsplit  11967  sumsnf  11969  fsumsplitsn  11970  sumtp  11974  sumsplitdc  11992  fsum2dlemstep  11994  fisum0diag2  12007  fsumconst  12014  modfsummodlemstep  12017  fsum00  12022  fsumabs  12025  fsumiun  12037  isumlessdc  12056  expcnv  12064  prodmodc  12138  zproddc  12139  iprodap  12140  iprodap0  12142  fprodssdc  12150  prodsnf  12152  fprodsplitdc  12156  fprodsplit  12157  fprodm1  12158  fprod1p  12159  fprodunsn  12164  fprod2dlemstep  12182  fprodsplitsn  12193  ef0lem  12220  modmulconst  12383  dvdsdivcl  12410  dvdsssfz1  12412  dvdsfac  12420  zeoxor  12429  nn0ehalf  12463  nn0oddm1d2  12469  nnoddm1d2  12470  divalglemeunn  12481  divalglemeuneg  12483  bitsfzolem  12514  bitsinv1  12522  gcdsupex  12527  gcdsupcl  12528  bezoutlemnewy  12566  bezoutlemmain  12568  bezoutlemeu  12577  dfgcd2  12584  nnwosdc  12609  nninfct  12611  algrf  12616  algcvgblem  12620  lcmgcdlem  12648  lcmdvds  12650  coprmgcdb  12659  mulgcddvds  12665  qredeu  12668  cncongr1  12674  cncongr2  12675  isprm2lem  12687  dvdsnprmd  12696  prmdc  12701  oddprmge3  12706  pw2dvdseu  12739  phibndlem  12787  dfphi2  12791  hashdvds  12792  phiprmpw  12793  eulerthlemh  12802  hashgcdeq  12811  phisum  12812  odzdvds  12817  reumodprminv  12825  nnnn0modprm0  12827  prm23ge5  12836  pclemdc  12860  pcdvdsb  12892  difsqpwdvds  12910  oddprmdvds  12926  1arith  12939  4sqlem3  12962  4sqlemafi  12967  4sqlemffi  12968  4sqleminfi  12969  4sqexercise1  12970  4sqlem11  12973  4sqlem19  12981  ennnfonelemdc  13019  ennnfonelemh  13024  ennnfonelemhf1o  13033  ennnfonelemf1  13038  ennnfonelemrn  13039  ennnfonelemdm  13040  exmidunben  13046  ctinfomlemom  13047  ctinfom  13048  ctiunctlemudc  13057  ctiunctlemf  13058  ctiunctal  13061  nninfdclemcl  13068  nninfdclemf  13069  nninfdclemp1  13070  isstructim  13095  setsresg  13119  strleund  13185  1strbas  13199  2strbasg  13202  2stropg  13203  restsspw  13331  tgval  13344  ptex  13346  imasaddfnlemg  13396  fnpr2o  13421  fnpr2ob  13422  mgmidsssn0  13466  fngsum  13470  igsumvalx  13471  isnsgrp  13488  sgrpidmndm  13502  mndinvmod  13527  mnd1  13537  mhmeql  13574  grpinveu  13620  prdsinvlem  13690  mulgval  13708  subgintm  13784  trivsubgsnd  13787  eqgfval  13808  ecqusaddd  13824  ecqusaddcl  13825  ghmeql  13853  iscmnd  13884  imasabl  13922  gsumfzmhm2  13930  rnglz  13957  srgfcl  13985  rhmopp  14189  subrgdvds  14248  lssuni  14376  lssintclm  14397  lspf  14402  qusmulrng  14545  mulgrhm2  14623  znf1o  14664  psrbagfi  14686  psr1clfi  14701  mplsubgfilemcl  14712  istopon  14736  toponcom  14750  topgele  14752  topontopn  14760  tsettps  14761  eltg2b  14777  unitg  14785  tgss2  14802  bastop2  14807  distop  14808  epttop  14813  cldss2  14829  neisspw  14871  neipsm  14877  neiuni  14884  tgcn  14931  tgcnp  14932  cnntr  14948  lmff  14972  txuni2  14979  txbasex  14980  txbas  14981  txcnp  14994  txcnmpt  14996  txcn  14998  txdis  15000  txdis1cn  15001  cnmpt11  15006  cnmpt12  15010  cnmpt21  15014  cnmpt2t  15016  cnmpt22  15017  blsscls2  15216  xmetxpbl  15231  xmettxlem  15232  tgqioo  15278  fsumcncntop  15290  cncfmpt1f  15321  mulcncflem  15330  mulcncf  15331  dedekindeu  15346  dedekindicclemicc  15355  dedekindicc  15356  ivthinclemdisj  15363  hovercncf  15369  limcimo  15388  cnmptlimc  15397  reldvg  15402  dvfvalap  15404  dvfgg  15411  dvmptfsum  15448  dveflem  15449  dvef  15450  elply2  15458  sincn  15492  coscn  15493  reeff1o  15496  pilem3  15506  ioocosf1o  15577  mpodvdsmulf1o  15713  fsumdvdsmul  15714  perfectlem2  15723  lgsne0  15766  gausslemma2dlem1a  15786  gausslemma2dlem4  15792  lgseisenlem2  15799  lgseisenlem3  15800  lgsquadlem2  15806  2lgslem3  15829  2sqlem2  15843  mul2sq  15844  2sqlem3  15845  2sqlem7  15849  edgstruct  15914  pw0ss  15933  incistruhgr  15940  upgrex  15953  umgrnloop0  15967  upgr1een  15974  lfgrnloopen  15983  umgredg  15995  umgrnloop2  16001  uspgredgiedg  16028  uspgriedgedg  16029  usgrislfuspgrdom  16040  usgredg3  16064  uspgredg2vlem  16070  uspgredg2v  16071  ushgredgedg  16076  ushgredgedgloop  16078  uhgr0vsize0en  16085  usgr1e  16091  subusgr  16125  vtxedgfi  16139  vtxlpfi  16140  vtxdumgrfival  16148  1loopgrvd2fi  16155  p1evtxdeqfilem  16161  vdegp1aid  16164  wlkcprim  16200  wlk1walkdom  16209  uspgr2wlkeq  16215  upgr2wlkdc  16227  wlkres  16229  clwwlkccatlem  16250  clwwlknp  16267  umgr2cwwk2dif  16274  bj-trst  16335  bj-fast  16337  bj-stand  16344  bj-trdc  16348  bj-fadc  16350  decidr  16392  djulclALT  16397  djurclALT  16398  bj-charfunr  16405  bj-indind  16527  bj-2inf  16533  bj-nntrans2  16547  bj-peano4  16550  bj-nnord  16553  bj-inf2vn  16569  bj-inf2vn2  16570  bj-findis  16574  pwf1oexmid  16600  subctctexmid  16601  pw1dceq  16605  nnsf  16607  nninfsellemdc  16612  nninffeq  16622  nnnninfen  16623  exmidsbthrlem  16626  sbthom  16630  triap  16633  trilpo  16647  apdifflemr  16651  redcwlpo  16659  tridceq  16660  nconstwlpolem0  16667  nconstwlpolem  16669  nconstwlpo  16670  neapmkv  16672  ltlenmkv  16674