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  716  dcim  843  dcstab  846  stdcndc  847  stdcndcOLD  848  dcand  935  dcor  938  3mix1  1169  3mix2  1170  3jca  1180  syl3anbrc  1184  syl21anbrc  1185  inegd  1392  pclem6  1394  xoranor  1397  dcfrompeirce  1470  nfxfrd  1499  nfd  1547  hban  1571  nfan1  1588  nford  1591  nfand  1592  hbim1  1594  nfal  1600  alexim  1669  nnal  1673  ax6blem  1674  nf4r  1695  19.34  1708  nfexd  1785  sbcof2  1834  nfsb2or  1861  sbidm  1875  nfdv  1901  nfd2  2051  nfeudv  2070  mon  2084  eumo  2087  mo23  2096  eu2  2099  eu3h  2100  exmodc  2105  exmonim  2106  mo2r  2107  mo3h  2108  bm1.1  2191  eqrdv  2204  3eltr4g  2292  abbi2dv  2325  abbi1dv  2326  nfcd  2344  nfcxfrd  2347  dcned  2383  neqned  2384  3netr4g  2412  necon3bi  2427  necon2ai  2431  nnral  2497  alral  2552  rspe  2556  rsp2e  2558  rgen2a  2561  ralrimi  2578  r19.27v  2634  r19.28v  2635  r19.27av  2642  r19.32r  2653  nfreudxy  2681  mormo  2723  nrexrmo  2728  cgsex2g  2810  cgsex4g  2811  spc2egv  2867  spc2gv  2868  spc3egv  2869  spc3gv  2870  rspce  2876  ceqex  2904  elrab3t  2932  elrabd  2935  mosubt  2954  mo2icl  2956  reu3  2967  reu6i  2968  2rmorex  2983  sbc5  3026  rspesbca  3087  rmo2ilem  3092  sbnfc2  3158  ssrd  3202  ssrdv  3203  3sstr4g  3240  eqsstrid  3243  ss2abdv  3270  abssdv  3271  rabssdv  3277  ss2rabdv  3278  ssun1  3340  unssad  3354  unssbd  3355  ssddif  3411  uneqin  3428  indifdir  3433  undif3ss  3438  reuss2  3457  n0rf  3477  reximdva0m  3480  rabxmdc  3496  ssindif0im  3524  minel  3526  ralidm  3565  ralm  3568  dcun  3574  ifmdc  3617  disjsn2  3701  absneu  3710  rabsneu  3711  opprc  3849  elunii  3864  dfnfc2  3877  uniss2  3890  unidif  3891  ssunieq  3892  intab  3923  iunss2  3981  iunssd  3982  iunxdif2  3985  invdisj  4047  disjiun  4049  3brtr4g  4088  trin  4163  triun  4166  truni  4167  trint  4168  iinexgm  4209  class2seteq  4218  pwuni  4247  exmid1dc  4255  exmidn0m  4256  exmidsssn  4257  exmid0el  4259  exmidel  4260  exmidundif  4261  exmidundifim  4262  exmid1stab  4263  mss  4283  copsex2t  4302  euotd  4312  pwunim  4346  ispod  4364  sotricim  4383  exse  4396  frind  4412  trssord  4440  suctr  4481  pwnex  4509  eusvnf  4513  eusvnfb  4514  eusv2nf  4516  rexxfrd  4523  ralxfr2d  4524  rexxfr2d  4525  rabxfrd  4529  reuhypd  4531  eldifpw  4537  iunpw  4540  ssorduni  4548  onsucb  4564  onsucelsucr  4569  sucunielr  4571  ontriexmidim  4583  ordtri2or2exmidlem  4587  onsucelsucexmid  4591  reg2exmidlema  4595  setindel  4599  elirr  4602  orddisj  4607  en2lp  4615  suc11g  4618  ordsuc  4624  nlimsucg  4627  ordtri2or2exmid  4632  ontri2orexmidim  4633  zfregfr  4635  wessep  4639  tfi  4643  peano5  4659  limom  4675  peano2b  4676  nndceq0  4679  nnpredcl  4684  0nelrel  4734  eqrelrdv  4784  xpsspw  4800  relint  4812  relop  4841  eqbrrdva  4861  ssrelrn  4883  opeldm  4895  elres  5009  relssres  5011  elrelimasn  5062  exse2  5070  issref  5079  trin2  5088  dminss  5111  imainss  5112  rnxpid  5131  dmsn0el  5166  dmmptg  5194  relrelss  5223  cnviinm  5238  iotanul  5261  sniota  5276  dffun5r  5297  funmo  5300  funco  5325  funun  5329  fununmo  5330  fununfun  5331  funprg  5338  funtpg  5339  funtp  5341  fntpg  5344  fununi  5356  funcnvuni  5357  imadiflem  5367  imainlem  5369  funimaexglem  5371  isarep2  5375  fnunsn  5397  2elresin  5401  fnimadisj  5411  dmmptd  5421  fco  5456  funssxp  5460  fssres  5468  feu  5475  fimacnvdisj  5477  fabexg  5480  f00  5484  f0rn0  5487  f1co  5510  fores  5525  foco  5526  f1ores  5554  foimacnv  5557  f1oun  5559  fun11iun  5560  f1oco  5562  fo00  5576  brprcneu  5587  fv3  5617  relelfvdm  5626  nfvres  5628  nfunsn  5629  funfvbrb  5711  respreima  5726  dff2  5742  dff3im  5743  dffo4  5746  fvmptelcdm  5751  ffvresb  5761  f1oresrab  5763  fmptco  5764  fsn  5770  fpr  5784  ftpg  5786  fsnunf  5802  fsnunfv  5803  elabrex  5844  dff1o6  5863  foeqcnvco  5877  fliftel1  5881  isores1  5901  isoini2  5906  riotasbc  5933  acexmidlemph  5955  acexmidlemcase  5957  oprabidlem  5993  brabvv  6009  eloprabga  6050  fnoprabg  6064  caovimo  6158  oprabexd  6230  uchoice  6241  fo1stresm  6265  fo2ndresm  6266  unielxp  6278  1st2ndbr  6288  fmpoco  6320  1stconst  6325  2ndconst  6326  poxp  6336  spc2ed  6337  disjxp1  6340  reldmtpos  6357  tposfun  6364  dftpos4  6367  smores  6396  smores2  6398  tfrlem1  6412  tfr0dm  6426  tfrlemibxssdm  6431  tfrlemibex  6433  tfrlemiubacc  6434  tfrlemi14d  6437  tfrexlem  6438  tfri1d  6439  tfr1onlembxssdm  6447  tfr1onlembex  6449  tfr1onlemubacc  6450  tfr1onlemres  6453  tfrcllemsucfn  6457  tfrcllembxssdm  6460  tfrcllembex  6462  tfrcllemubacc  6463  tfrcllemres  6466  tfri3  6471  rdgon  6490  frecabcl  6503  frecfcllem  6508  frecrdg  6512  2oconcl  6543  nnsucelsuc  6595  nntri3or  6597  nndceq  6603  nndcel  6604  dcdifsnid  6608  ecexr  6643  brdifun  6665  ecelqsdm  6710  iinerm  6712  eroveu  6731  erovlem  6732  ecopovtrn  6737  ecopovtrng  6740  th3qlem1  6742  pmsspw  6788  map0b  6792  mapsn  6795  mapsncnv  6800  ixpf  6825  uniixp  6826  ixpexgg  6827  resixp  6838  f1oen3g  6863  ssdomg  6888  domtr  6895  snfig  6925  enpr2d  6930  xpf1o  6961  xpmapenlem  6966  php5dom  6980  fidceq  6987  nnfi  6990  fiunsnnn  6999  findcard  7006  findcard2  7007  findcard2s  7008  ac6sfi  7016  tridc  7017  fimax2gtri  7019  finexdc  7020  exmidpw  7026  exmidpweq  7027  exmidpw2en  7030  nnwetri  7034  unsnfi  7037  unsnfidcex  7038  unsnfidcel  7039  undifdcss  7041  tpfidisj  7047  tpfidceq  7048  iunfidisj  7069  snexxph  7073  fidcenumlemrks  7076  sbthlem2  7081  sbthlemi3  7082  sbthlem7  7086  sbthlemi8  7087  fival  7093  dcfi  7104  supmoti  7116  djuss  7193  updjudhf  7202  updjud  7205  casefun  7208  caseinj  7212  omp1eomlem  7217  djufun  7227  djuinj  7229  ctssdccl  7234  ctfoex  7241  nnnninf  7249  nnnninfeq2  7252  nninfisollem0  7253  nninfisollemne  7254  nninfisollemeq  7255  nninfisol  7256  finomni  7263  exmidomniim  7264  exmidomni  7265  fodjuomnilemdc  7267  omniwomnimkv  7290  nninfdcinf  7294  nninfwlporlem  7296  nninfwlpoimlemg  7298  nninfwlpoim  7302  nninfinfwlpo  7303  exmidonfinlem  7327  exmidfodomrlemr  7336  exmidfodomrlemrALT  7337  finacn  7342  exmidaclem  7346  dju1en  7351  exmidontriimlem1  7359  exmidontriimlem3  7361  iftrueb01  7364  pw1on  7367  3nsssucpw1  7377  2omotaplemap  7399  2omotap  7401  exmidmotap  7403  cc4f  7411  cc4n  7413  acnccim  7414  dmaddpqlem  7520  nqpi  7521  dmaddpq  7522  dmmulpq  7523  ltdcnq  7540  subhalfnqq  7557  enq0sym  7575  enq0ref  7576  enq0tr  7577  nqnq0pi  7581  nq0nn  7585  addnq0mo  7590  mulnq0mo  7591  nqpnq0nq  7596  nqnq0a  7597  nqnq0m  7598  npsspw  7614  elnp1st2nd  7619  prnmaxl  7631  prnminu  7632  prarloc  7646  genprndl  7664  genprndu  7665  nqprm  7685  nqprl  7694  nqpru  7695  addnqprlemrl  7700  addnqprlemru  7701  prmuloc  7709  mulnqprlemrl  7716  mulnqprlemru  7717  ltsopr  7739  ltexprlemm  7743  ltexprlemopl  7744  ltexprlemopu  7746  lteupri  7760  recexprlemopl  7768  recexprlemopu  7770  recexprlemdisj  7773  archpr  7786  cauappcvgprlemdisj  7794  cauappcvgprlemladdrl  7800  cauappcvgprlem2  7803  caucvgprlemnbj  7810  caucvgprlemdisj  7817  caucvgprlemladdfu  7820  caucvgprlem2  7823  caucvgprprlemnbj  7836  caucvgprprlemdisj  7845  suplocexprlemml  7859  suplocexprlemrl  7860  suplocexprlemmu  7861  suplocexprlemloc  7864  addsrmo  7886  mulsrmo  7887  recexgt0sr  7916  prsrpos  7928  caucvgsrlemasr  7933  suplocsrlemb  7949  suplocsrlempr  7950  suplocsr  7952  elrealeu  7972  pitonn  7991  pitoregt0  7992  pitore  7993  recnnre  7994  axaddcl  8007  axaddrcl  8008  axmulcl  8009  axmulrcl  8010  axrnegex  8022  axcnre  8024  axpre-lttrn  8027  rereceu  8032  axarch  8034  axpre-suploclemres  8044  axpre-suploc  8045  ltxrlt  8168  apirr  8708  divmulasscomap  8799  rerecclap  8833  lbreu  9048  arch  9322  0mnnnnn0  9357  nnm1nn0  9366  elnnnn0c  9370  elnnz1  9425  ztri3or0  9444  nzadd  9455  nn0n0n1ge2  9473  zdceq  9478  zdcle  9479  zdclt  9480  uzind  9514  eluzge3nn  9723  supinfneg  9746  infsupneg  9747  eluz2b2  9754  elnn1uz2  9758  elnn0dc  9762  elnndc  9763  nn01to3  9768  znq  9775  qaddcl  9786  qmulcl  9788  qreccl  9793  irradd  9797  irrmul  9798  elpq  9800  cnref1o  9802  xnn0dcle  9954  xrpnfdc  9994  xrmnfdc  9995  xaddcom  10013  xnegdi  10020  xpncan  10023  xleadd1a  10025  iooidg  10061  elioo4g  10086  elfzd  10168  fzdcel  10192  fznlem  10193  fzpreddisj  10223  fz0to4untppr  10276  elfz0ubfz0  10277  elfz0fzfz0  10278  fz0fzelfz0  10279  fz0fzdiffz0  10282  elfzmlbp  10284  difelfzle  10286  4fvwrd4  10292  fzosplit  10331  elfzo0  10338  fzo1fzo0n0  10339  elfzonn0  10342  fzofzim  10344  elfzo1  10346  elfzom1elp1fzo  10363  fzossfzop1  10373  ssfzo12bi  10386  exfzdc  10401  zsupcllemstep  10404  infssuzex  10408  qdceq  10419  qdclt  10420  exbtwnzlemstep  10422  exbtwnzlemex  10424  exbtwnz  10425  rebtwn2zlemstep  10427  rebtwn2z  10429  qbtwnxr  10432  modfzo0difsn  10572  frec2uzrand  10582  frec2uzf1od  10583  frecuzrdgrcl  10587  frecuzrdgtcl  10589  frecuzrdgrclt  10592  frecuzrdgfunlem  10596  frecfzennn  10603  nninfinf  10620  seq3f1olemp  10692  seq3f1oleml  10693  seqf1oglem1  10696  ser0f  10711  expcl2lemap  10728  hashunsng  10984  iswrdinn0  11031  snopiswrd  11036  wrdlndm  11043  iswrdsymb  11044  wrdsymb1  11062  ccatfv0  11092  ccatval21sw  11094  lswccatn0lsw  11100  eqs1  11115  ccat1st1st  11126  lswccats1fst  11129  fzowrddc  11133  swrdfv0  11140  swrdlen2  11148  swrdfv2  11149  swrdsbslen  11152  swrdspsleq  11153  pfxfv0  11178  pfxtrcfv0  11180  pfxeq  11182  pfx1  11189  swrdswrdlem  11190  cats1un  11207  shftfvalg  11214  shftfval  11217  caucvgre  11377  rexanuz  11384  recvguniq  11391  rennim  11398  resqrexlemf  11403  rsqrmo  11423  fimaxre2  11623  climeu  11692  sumdc  11754  summodc  11779  zsumdc  11780  isum  11781  fisumss  11788  isumss2  11789  fsumsplit  11803  sumsnf  11805  fsumsplitsn  11806  sumtp  11810  sumsplitdc  11828  fsum2dlemstep  11830  fisum0diag2  11843  fsumconst  11850  modfsummodlemstep  11853  fsum00  11858  fsumabs  11861  fsumiun  11873  isumlessdc  11892  expcnv  11900  prodmodc  11974  zproddc  11975  iprodap  11976  iprodap0  11978  fprodssdc  11986  prodsnf  11988  fprodsplitdc  11992  fprodsplit  11993  fprodm1  11994  fprod1p  11995  fprodunsn  12000  fprod2dlemstep  12018  fprodsplitsn  12029  ef0lem  12056  modmulconst  12219  dvdsdivcl  12246  dvdsssfz1  12248  dvdsfac  12256  zeoxor  12265  nn0ehalf  12299  nn0oddm1d2  12305  nnoddm1d2  12306  divalglemeunn  12317  divalglemeuneg  12319  bitsfzolem  12350  bitsinv1  12358  gcdsupex  12363  gcdsupcl  12364  bezoutlemnewy  12402  bezoutlemmain  12404  bezoutlemeu  12413  dfgcd2  12420  nnwosdc  12445  nninfct  12447  algrf  12452  algcvgblem  12456  lcmgcdlem  12484  lcmdvds  12486  coprmgcdb  12495  mulgcddvds  12501  qredeu  12504  cncongr1  12510  cncongr2  12511  isprm2lem  12523  dvdsnprmd  12532  prmdc  12537  oddprmge3  12542  pw2dvdseu  12575  phibndlem  12623  dfphi2  12627  hashdvds  12628  phiprmpw  12629  eulerthlemh  12638  hashgcdeq  12647  phisum  12648  odzdvds  12653  reumodprminv  12661  nnnn0modprm0  12663  prm23ge5  12672  pclemdc  12696  pcdvdsb  12728  difsqpwdvds  12746  oddprmdvds  12762  1arith  12775  4sqlem3  12798  4sqlemafi  12803  4sqlemffi  12804  4sqleminfi  12805  4sqexercise1  12806  4sqlem11  12809  4sqlem19  12817  ennnfonelemdc  12855  ennnfonelemh  12860  ennnfonelemhf1o  12869  ennnfonelemf1  12874  ennnfonelemrn  12875  ennnfonelemdm  12876  exmidunben  12882  ctinfomlemom  12883  ctinfom  12884  ctiunctlemudc  12893  ctiunctlemf  12894  ctiunctal  12897  nninfdclemcl  12904  nninfdclemf  12905  nninfdclemp1  12906  isstructim  12931  setsresg  12955  strleund  13020  1strbas  13034  2strbasg  13037  2stropg  13038  restsspw  13166  tgval  13179  ptex  13181  imasaddfnlemg  13231  fnpr2o  13256  fnpr2ob  13257  mgmidsssn0  13301  fngsum  13305  igsumvalx  13306  isnsgrp  13323  sgrpidmndm  13337  mndinvmod  13362  mnd1  13372  mhmeql  13409  grpinveu  13455  prdsinvlem  13525  mulgval  13543  subgintm  13619  trivsubgsnd  13622  eqgfval  13643  ecqusaddd  13659  ecqusaddcl  13660  ghmeql  13688  iscmnd  13719  imasabl  13757  gsumfzmhm2  13765  rnglz  13792  srgfcl  13820  reldvdsrsrg  13939  rhmopp  14023  subrgdvds  14082  lssuni  14210  lssintclm  14231  lspf  14236  qusmulrng  14379  mulgrhm2  14457  znf1o  14498  psrbagfi  14520  psr1clfi  14535  mplsubgfilemcl  14546  istopon  14570  toponcom  14584  topgele  14586  topontopn  14594  tsettps  14595  eltg2b  14611  unitg  14619  tgss2  14636  bastop2  14641  distop  14642  epttop  14647  cldss2  14663  neisspw  14705  neipsm  14711  neiuni  14718  tgcn  14765  tgcnp  14766  cnntr  14782  lmff  14806  txuni2  14813  txbasex  14814  txbas  14815  txcnp  14828  txcnmpt  14830  txcn  14832  txdis  14834  txdis1cn  14835  cnmpt11  14840  cnmpt12  14844  cnmpt21  14848  cnmpt2t  14850  cnmpt22  14851  blsscls2  15050  xmetxpbl  15065  xmettxlem  15066  tgqioo  15112  fsumcncntop  15124  cncfmpt1f  15155  mulcncflem  15164  mulcncf  15165  dedekindeu  15180  dedekindicclemicc  15189  dedekindicc  15190  ivthinclemdisj  15197  hovercncf  15203  limcimo  15222  cnmptlimc  15231  reldvg  15236  dvfvalap  15238  dvfgg  15245  dvmptfsum  15282  dveflem  15283  dvef  15284  elply2  15292  sincn  15326  coscn  15327  reeff1o  15330  pilem3  15340  ioocosf1o  15411  mpodvdsmulf1o  15547  fsumdvdsmul  15548  perfectlem2  15557  lgsne0  15600  gausslemma2dlem1a  15620  gausslemma2dlem4  15626  lgseisenlem2  15633  lgseisenlem3  15634  lgsquadlem2  15640  2lgslem3  15663  2sqlem2  15677  mul2sq  15678  2sqlem3  15679  2sqlem7  15683  edgstruct  15745  pw0ss  15764  incistruhgr  15771  upgrex  15784  lfgrnloopen  15809  umgredg  15819  umgrnloop2  15825  bj-trst  15845  bj-fast  15847  bj-stand  15854  bj-trdc  15858  bj-fadc  15860  decidr  15902  djulclALT  15907  djurclALT  15908  bj-charfunr  15915  bj-indind  16037  bj-2inf  16043  bj-nntrans2  16057  bj-peano4  16060  bj-nnord  16063  bj-inf2vn  16079  bj-inf2vn2  16080  bj-findis  16084  dom1o  16098  pwf1oexmid  16108  subctctexmid  16109  nnsf  16114  nninfsellemdc  16119  nninffeq  16129  nnnninfen  16130  exmidsbthrlem  16133  sbthom  16137  triap  16140  trilpo  16154  apdifflemr  16158  redcwlpo  16166  tridceq  16167  nconstwlpolem0  16174  nconstwlpolem  16176  nconstwlpo  16177  neapmkv  16179  ltlenmkv  16181