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  oibabs  714  dcim  841  dcstab  844  stdcndc  845  stdcndcOLD  846  dcor  935  3mix1  1166  3mix2  1167  3jca  1177  syl3anbrc  1181  syl21anbrc  1182  inegd  1372  pclem6  1374  xoranor  1377  nfxfrd  1475  nfd  1523  hban  1547  nfan1  1564  nford  1567  nfand  1568  hbim1  1570  nfal  1576  alexim  1645  nnal  1649  ax6blem  1650  nf4r  1671  19.34  1684  nfexd  1761  sbcof2  1810  nfsb2or  1837  sbidm  1851  nfdv  1877  nfd2  2022  nfeudv  2041  mon  2055  eumo  2058  mo23  2067  eu2  2070  eu3h  2071  exmodc  2076  exmonim  2077  mo2r  2078  mo3h  2079  bm1.1  2162  eqrdv  2175  3eltr4g  2263  abbi2dv  2296  abbi1dv  2297  nfcd  2314  nfcxfrd  2317  dcned  2353  neqned  2354  3netr4g  2382  necon3bi  2397  necon2ai  2401  nnral  2467  alral  2522  rspe  2526  rsp2e  2528  rgen2a  2531  ralrimi  2548  r19.27v  2604  r19.28v  2605  r19.27av  2612  r19.32r  2623  nfreudxy  2651  mormo  2689  nrexrmo  2694  cgsex2g  2774  cgsex4g  2775  spc2egv  2828  spc2gv  2829  spc3egv  2830  spc3gv  2831  rspce  2837  ceqex  2865  elrab3t  2893  elrabd  2896  mosubt  2915  mo2icl  2917  reu3  2928  reu6i  2929  2rmorex  2944  sbc5  2987  rspesbca  3048  rmo2ilem  3053  sbnfc2  3118  ssrd  3161  ssrdv  3162  3sstr4g  3199  eqsstrid  3202  ss2abdv  3229  abssdv  3230  rabssdv  3236  ss2rabdv  3237  ssun1  3299  unssad  3313  unssbd  3314  ssddif  3370  uneqin  3387  indifdir  3392  undif3ss  3397  reuss2  3416  n0rf  3436  reximdva0m  3439  rabxmdc  3455  ssindif0im  3483  minel  3485  ralidm  3524  ralm  3528  dcun  3534  ifmdc  3575  disjsn2  3656  absneu  3665  rabsneu  3666  opprc  3800  elunii  3815  dfnfc2  3828  uniss2  3841  unidif  3842  ssunieq  3843  intab  3874  iunss2  3932  iunssd  3933  iunxdif2  3936  invdisj  3998  disjiun  3999  3brtr4g  4038  trin  4112  triun  4115  truni  4116  trint  4117  iinexgm  4155  class2seteq  4164  pwuni  4193  exmid1dc  4201  exmidn0m  4202  exmidsssn  4203  exmid0el  4205  exmidel  4206  exmidundif  4207  exmidundifim  4208  exmid1stab  4209  mss  4227  copsex2t  4246  euotd  4255  pwunim  4287  ispod  4305  sotricim  4324  exse  4337  frind  4353  trssord  4381  suctr  4422  pwnex  4450  eusvnf  4454  eusvnfb  4455  eusv2nf  4457  rexxfrd  4464  ralxfr2d  4465  rexxfr2d  4466  rabxfrd  4470  reuhypd  4472  eldifpw  4478  iunpw  4481  ssorduni  4487  onsucb  4503  onsucelsucr  4508  sucunielr  4510  ontriexmidim  4522  ordtri2or2exmidlem  4526  onsucelsucexmid  4530  reg2exmidlema  4534  setindel  4538  elirr  4541  orddisj  4546  en2lp  4554  suc11g  4557  ordsuc  4563  nlimsucg  4566  ordtri2or2exmid  4571  ontri2orexmidim  4572  zfregfr  4574  wessep  4578  tfi  4582  peano5  4598  limom  4614  peano2b  4615  nndceq0  4618  nnpredcl  4623  0nelrel  4673  eqrelrdv  4723  xpsspw  4739  relint  4751  relop  4778  eqbrrdva  4798  opeldm  4831  elres  4944  relssres  4946  elrelimasn  4995  exse2  5003  issref  5012  trin2  5021  dminss  5044  imainss  5045  rnxpid  5064  dmsn0el  5099  dmmptg  5127  relrelss  5156  cnviinm  5171  iotanul  5194  sniota  5208  dffun5r  5229  funmo  5232  funco  5257  funun  5261  funprg  5267  funtpg  5268  funtp  5270  fntpg  5273  fununi  5285  funcnvuni  5286  imadiflem  5296  imainlem  5298  funimaexglem  5300  isarep2  5304  fnunsn  5324  2elresin  5328  fnimadisj  5337  dmmptd  5347  fco  5382  funssxp  5386  fssres  5392  feu  5399  fimacnvdisj  5401  fabexg  5404  f00  5408  f0rn0  5411  f1co  5434  fores  5448  foco  5449  f1ores  5477  foimacnv  5480  f1oun  5482  fun11iun  5483  f1oco  5485  fo00  5498  brprcneu  5509  fv3  5539  relelfvdm  5548  nfvres  5549  nfunsn  5550  funfvbrb  5630  respreima  5645  dff2  5661  dff3im  5662  dffo4  5665  fvmptelcdm  5670  ffvresb  5680  f1oresrab  5682  fmptco  5683  fsn  5689  fpr  5699  ftpg  5701  fsnunf  5717  fsnunfv  5718  elabrex  5759  dff1o6  5777  foeqcnvco  5791  fliftel1  5795  isores1  5815  isoini2  5820  riotasbc  5846  acexmidlemph  5868  acexmidlemcase  5870  oprabidlem  5906  brabvv  5921  eloprabga  5962  fnoprabg  5976  caovimo  6068  oprabexd  6128  fo1stresm  6162  fo2ndresm  6163  unielxp  6175  1st2ndbr  6185  fmpoco  6217  1stconst  6222  2ndconst  6223  poxp  6233  spc2ed  6234  disjxp1  6237  reldmtpos  6254  tposfun  6261  dftpos4  6264  smores  6293  smores2  6295  tfrlem1  6309  tfr0dm  6323  tfrlemibxssdm  6328  tfrlemibex  6330  tfrlemiubacc  6331  tfrlemi14d  6334  tfrexlem  6335  tfri1d  6336  tfr1onlembxssdm  6344  tfr1onlembex  6346  tfr1onlemubacc  6347  tfr1onlemres  6350  tfrcllemsucfn  6354  tfrcllembxssdm  6357  tfrcllembex  6359  tfrcllemubacc  6360  tfrcllemres  6363  tfri3  6368  rdgon  6387  frecabcl  6400  frecfcllem  6405  frecrdg  6409  2oconcl  6440  nnsucelsuc  6492  nntri3or  6494  nndceq  6500  nndcel  6501  dcdifsnid  6505  ecexr  6540  brdifun  6562  ecelqsdm  6605  iinerm  6607  eroveu  6626  erovlem  6627  ecopovtrn  6632  ecopovtrng  6635  th3qlem1  6637  pmsspw  6683  map0b  6687  mapsn  6690  mapsncnv  6695  ixpf  6720  uniixp  6721  ixpexgg  6722  resixp  6733  f1oen3g  6754  ssdomg  6778  domtr  6785  snfig  6814  enpr2d  6817  xpf1o  6844  xpmapenlem  6849  php5dom  6863  fidceq  6869  nnfi  6872  fiunsnnn  6881  findcard  6888  findcard2  6889  findcard2s  6890  ac6sfi  6898  tridc  6899  fimax2gtri  6901  finexdc  6902  exmidpw  6908  exmidpweq  6909  nnwetri  6915  unsnfi  6918  unsnfidcex  6919  unsnfidcel  6920  undifdcss  6922  tpfidisj  6927  iunfidisj  6945  snexxph  6949  fidcenumlemrks  6952  sbthlem2  6957  sbthlemi3  6958  sbthlem7  6962  sbthlemi8  6963  fival  6969  dcfi  6980  supmoti  6992  djuss  7069  updjudhf  7078  updjud  7081  casefun  7084  caseinj  7088  omp1eomlem  7093  djufun  7103  djuinj  7105  ctssdccl  7110  ctfoex  7117  nnnninf  7124  nnnninfeq2  7127  nninfisollem0  7128  nninfisollemne  7129  nninfisollemeq  7130  nninfisol  7131  finomni  7138  exmidomniim  7139  exmidomni  7140  fodjuomnilemdc  7142  omniwomnimkv  7165  nninfdcinf  7169  nninfwlporlem  7171  nninfwlpoimlemg  7173  nninfwlpoim  7176  exmidonfinlem  7192  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidaclem  7207  dju1en  7212  exmidontriimlem1  7220  exmidontriimlem3  7222  pw1on  7225  3nsssucpw1  7235  2omotaplemap  7256  2omotap  7258  exmidmotap  7260  cc4f  7268  cc4n  7270  dmaddpqlem  7376  nqpi  7377  dmaddpq  7378  dmmulpq  7379  ltdcnq  7396  subhalfnqq  7413  enq0sym  7431  enq0ref  7432  enq0tr  7433  nqnq0pi  7437  nq0nn  7441  addnq0mo  7446  mulnq0mo  7447  nqpnq0nq  7452  nqnq0a  7453  nqnq0m  7454  npsspw  7470  elnp1st2nd  7475  prnmaxl  7487  prnminu  7488  prarloc  7502  genprndl  7520  genprndu  7521  nqprm  7541  nqprl  7550  nqpru  7551  addnqprlemrl  7556  addnqprlemru  7557  prmuloc  7565  mulnqprlemrl  7572  mulnqprlemru  7573  ltsopr  7595  ltexprlemm  7599  ltexprlemopl  7600  ltexprlemopu  7602  lteupri  7616  recexprlemopl  7624  recexprlemopu  7626  recexprlemdisj  7629  archpr  7642  cauappcvgprlemdisj  7650  cauappcvgprlemladdrl  7656  cauappcvgprlem2  7659  caucvgprlemnbj  7666  caucvgprlemdisj  7673  caucvgprlemladdfu  7676  caucvgprlem2  7679  caucvgprprlemnbj  7692  caucvgprprlemdisj  7701  suplocexprlemml  7715  suplocexprlemrl  7716  suplocexprlemmu  7717  suplocexprlemloc  7720  addsrmo  7742  mulsrmo  7743  recexgt0sr  7772  prsrpos  7784  caucvgsrlemasr  7789  suplocsrlemb  7805  suplocsrlempr  7806  suplocsr  7808  elrealeu  7828  pitonn  7847  pitoregt0  7848  pitore  7849  recnnre  7850  axaddcl  7863  axaddrcl  7864  axmulcl  7865  axmulrcl  7866  axrnegex  7878  axcnre  7880  axpre-lttrn  7883  rereceu  7888  axarch  7890  axpre-suploclemres  7900  axpre-suploc  7901  ltxrlt  8023  apirr  8562  divmulasscomap  8653  rerecclap  8687  lbreu  8902  arch  9173  0mnnnnn0  9208  nnm1nn0  9217  elnnnn0c  9221  elnnz1  9276  ztri3or0  9295  nzadd  9305  nn0n0n1ge2  9323  zdceq  9328  zdcle  9329  zdclt  9330  uzind  9364  eluzge3nn  9572  supinfneg  9595  infsupneg  9596  eluz2b2  9603  elnn1uz2  9607  elnn0dc  9611  elnndc  9612  nn01to3  9617  znq  9624  qaddcl  9635  qmulcl  9637  qreccl  9642  irradd  9646  irrmul  9647  elpq  9648  cnref1o  9650  xnn0dcle  9802  xrpnfdc  9842  xrmnfdc  9843  xaddcom  9861  xnegdi  9868  xpncan  9871  xleadd1a  9873  iooidg  9909  elioo4g  9934  elfzd  10016  fzdcel  10040  fznlem  10041  fzpreddisj  10071  fz0to4untppr  10124  elfz0ubfz0  10125  elfz0fzfz0  10126  fz0fzelfz0  10127  fz0fzdiffz0  10130  elfzmlbp  10132  difelfzle  10134  4fvwrd4  10140  fzosplit  10177  elfzo0  10182  fzo1fzo0n0  10183  elfzonn0  10186  fzofzim  10188  elfzo1  10190  elfzom1elp1fzo  10202  fzossfzop1  10212  ssfzo12bi  10225  exfzdc  10240  qdceq  10247  exbtwnzlemstep  10248  exbtwnzlemex  10250  exbtwnz  10251  rebtwn2zlemstep  10253  rebtwn2z  10255  qbtwnxr  10258  modfzo0difsn  10395  frec2uzrand  10405  frec2uzf1od  10406  frecuzrdgrcl  10410  frecuzrdgtcl  10412  frecuzrdgrclt  10415  frecuzrdgfunlem  10419  frecfzennn  10426  seq3f1olemp  10502  seq3f1oleml  10503  ser0f  10515  expcl2lemap  10532  hashunsng  10787  shftfvalg  10827  shftfval  10830  caucvgre  10990  rexanuz  10997  recvguniq  11004  rennim  11011  resqrexlemf  11016  rsqrmo  11036  fimaxre2  11235  climeu  11304  sumdc  11366  summodc  11391  zsumdc  11392  isum  11393  fisumss  11400  isumss2  11401  fsumsplit  11415  sumsnf  11417  fsumsplitsn  11418  sumtp  11422  sumsplitdc  11440  fsum2dlemstep  11442  fisum0diag2  11455  fsumconst  11462  modfsummodlemstep  11465  fsum00  11470  fsumabs  11473  fsumiun  11485  isumlessdc  11504  expcnv  11512  prodmodc  11586  zproddc  11587  iprodap  11588  iprodap0  11590  fprodssdc  11598  prodsnf  11600  fprodsplitdc  11604  fprodsplit  11605  fprodm1  11606  fprod1p  11607  fprodunsn  11612  fprod2dlemstep  11630  fprodsplitsn  11641  ef0lem  11668  modmulconst  11830  dvdsdivcl  11856  dvdsssfz1  11858  dvdsfac  11866  zeoxor  11874  nn0ehalf  11908  nn0oddm1d2  11914  nnoddm1d2  11915  divalglemeunn  11926  divalglemeuneg  11928  zsupcllemstep  11946  infssuzex  11950  gcdsupex  11958  gcdsupcl  11959  bezoutlemnewy  11997  bezoutlemmain  11999  bezoutlemeu  12008  dfgcd2  12015  nnwosdc  12040  algrf  12045  algcvgblem  12049  lcmgcdlem  12077  lcmdvds  12079  coprmgcdb  12088  mulgcddvds  12094  qredeu  12097  cncongr1  12103  cncongr2  12104  isprm2lem  12116  dvdsnprmd  12125  prmdc  12130  oddprmge3  12135  pw2dvdseu  12168  phibndlem  12216  dfphi2  12220  hashdvds  12221  phiprmpw  12222  eulerthlemh  12231  hashgcdeq  12239  phisum  12240  odzdvds  12245  reumodprminv  12253  nnnn0modprm0  12255  prm23ge5  12264  pclemdc  12288  pcdvdsb  12319  difsqpwdvds  12337  oddprmdvds  12352  1arith  12365  4sqlem3  12388  ennnfonelemdc  12400  ennnfonelemh  12405  ennnfonelemhf1o  12414  ennnfonelemf1  12419  ennnfonelemrn  12420  ennnfonelemdm  12421  exmidunben  12427  ctinfomlemom  12428  ctinfom  12429  ctiunctlemudc  12438  ctiunctlemf  12439  ctiunctal  12442  nninfdclemcl  12449  nninfdclemf  12450  nninfdclemp1  12451  isstructim  12476  setsresg  12500  strleund  12562  1strbas  12576  2strbasg  12578  2stropg  12579  restsspw  12698  tgval  12711  ptex  12713  imasaddfnlemg  12735  fnpr2o  12758  fnpr2ob  12759  mgmidsssn0  12803  isnsgrp  12812  sgrpidmndm  12821  mndinvmod  12846  mnd1  12847  mhmeql  12876  grpinveu  12911  mulgval  12986  subgintm  13058  trivsubgsnd  13061  eqgfval  13081  iscmnd  13101  srgfcl  13156  reldvdsrsrg  13261  subrgdvds  13356  istopon  13516  toponcom  13530  topgele  13532  topontopn  13540  tsettps  13541  eltg2b  13557  unitg  13565  tgss2  13582  bastop2  13587  distop  13588  epttop  13593  cldss2  13609  neisspw  13651  neipsm  13657  neiuni  13664  tgcn  13711  tgcnp  13712  cnntr  13728  lmff  13752  txuni2  13759  txbasex  13760  txbas  13761  txcnp  13774  txcnmpt  13776  txcn  13778  txdis  13780  txdis1cn  13781  cnmpt11  13786  cnmpt12  13790  cnmpt21  13794  cnmpt2t  13796  cnmpt22  13797  blsscls2  13996  xmetxpbl  14011  xmettxlem  14012  tgqioo  14050  fsumcncntop  14059  cncfmpt1f  14087  mulcncflem  14093  mulcncf  14094  dedekindeu  14104  dedekindicclemicc  14113  dedekindicc  14114  ivthinclemdisj  14121  limcimo  14137  cnmptlimc  14146  reldvg  14151  dvfvalap  14153  dvfgg  14160  dveflem  14190  dvef  14191  sincn  14193  coscn  14194  reeff1o  14197  pilem3  14207  ioocosf1o  14278  lgsne0  14442  lgseisenlem2  14454  2sqlem2  14465  mul2sq  14466  2sqlem3  14467  2sqlem7  14471  bj-trst  14494  bj-fast  14496  bj-stand  14503  bj-trdc  14507  bj-fadc  14509  decidr  14551  djulclALT  14556  djurclALT  14557  bj-charfunr  14565  bj-indind  14687  bj-2inf  14693  bj-nntrans2  14707  bj-peano4  14710  bj-nnord  14713  bj-inf2vn  14729  bj-inf2vn2  14730  bj-findis  14734  pwf1oexmid  14752  subctctexmid  14753  nnsf  14757  nninfsellemdc  14762  nninffeq  14772  exmidsbthrlem  14773  sbthom  14777  triap  14780  trilpo  14794  apdifflemr  14798  redcwlpo  14806  tridceq  14807  nconstwlpolem0  14813  nconstwlpolem  14815  nconstwlpo  14816  neapmkv  14818  ltlenmkv  14820