Theorem sylibr 133

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 132	. 2 |- ( ps -> ch )
4	1, 3	syl 14	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbbr  135  pm5.74rd  182  bitri  183  3imtr4i  200  sylanbrc  414  oibabs  704  dcim  831  dcstab  834  stdcndc  835  stdcndcOLD  836  dcor  925  3mix1  1156  3mix2  1157  3jca  1167  syl3anbrc  1171  syl21anbrc  1172  inegd  1362  pclem6  1364  xoranor  1367  nfxfrd  1463  nfd  1511  hban  1535  nfan1  1552  nford  1555  nfand  1556  hbim1  1558  nfal  1564  alexim  1633  nnal  1637  ax6blem  1638  nf4r  1659  19.34  1672  nfexd  1749  sbcof2  1798  nfsb2or  1825  sbidm  1839  nfdv  1865  nfd2  2010  nfeudv  2029  mon  2043  eumo  2046  mo23  2055  eu2  2058  eu3h  2059  exmodc  2064  exmonim  2065  mo2r  2066  mo3h  2067  bm1.1  2150  eqrdv  2163  3eltr4g  2252  abbi2dv  2285  abbi1dv  2286  nfcd  2303  nfcxfrd  2306  dcned  2342  neqned  2343  3netr4g  2371  necon3bi  2386  necon2ai  2390  nnral  2456  alral  2511  rspe  2515  rsp2e  2517  rgen2a  2520  ralrimi  2537  r19.27v  2593  r19.28v  2594  r19.27av  2601  r19.32r  2612  nfreudxy  2639  mormo  2677  nrexrmo  2682  cgsex2g  2762  cgsex4g  2763  spc2egv  2816  spc2gv  2817  spc3egv  2818  spc3gv  2819  rspce  2825  ceqex  2853  elrab3t  2881  elrabd  2884  mosubt  2903  mo2icl  2905  reu3  2916  reu6i  2917  2rmorex  2932  sbc5  2974  rspesbca  3035  rmo2ilem  3040  sbnfc2  3105  ssrd  3147  ssrdv  3148  3sstr4g  3185  eqsstrid  3188  ss2abdv  3215  abssdv  3216  rabssdv  3222  ss2rabdv  3223  ssun1  3285  unssad  3299  unssbd  3300  ssddif  3356  uneqin  3373  indifdir  3378  undif3ss  3383  reuss2  3402  n0rf  3421  reximdva0m  3424  rabxmdc  3440  ssindif0im  3468  minel  3470  ralidm  3509  ralm  3513  dcun  3519  ifmdc  3558  disjsn2  3639  absneu  3648  rabsneu  3649  opprc  3779  elunii  3794  dfnfc2  3807  uniss2  3820  unidif  3821  ssunieq  3822  intab  3853  iunss2  3911  iunxdif2  3914  invdisj  3976  disjiun  3977  3brtr4g  4016  trin  4090  triun  4093  truni  4094  trint  4095  iinexgm  4133  class2seteq  4142  pwuni  4171  exmid1dc  4179  exmidn0m  4180  exmidsssn  4181  exmid0el  4183  exmidel  4184  exmidundif  4185  exmidundifim  4186  mss  4204  copsex2t  4223  euotd  4232  pwunim  4264  ispod  4282  sotricim  4301  exse  4314  frind  4330  trssord  4358  suctr  4399  pwnex  4427  eusvnf  4431  eusvnfb  4432  eusv2nf  4434  rexxfrd  4441  ralxfr2d  4442  rexxfr2d  4443  rabxfrd  4447  reuhypd  4449  eldifpw  4455  iunpw  4458  ssorduni  4464  sucelon  4480  onsucelsucr  4485  sucunielr  4487  ontriexmidim  4499  ordtri2or2exmidlem  4503  onsucelsucexmid  4507  reg2exmidlema  4511  setindel  4515  elirr  4518  orddisj  4523  en2lp  4531  suc11g  4534  ordsuc  4540  nlimsucg  4543  ordtri2or2exmid  4548  ontri2orexmidim  4549  zfregfr  4551  wessep  4555  tfi  4559  peano5  4575  limom  4591  peano2b  4592  nndceq0  4595  nnpredcl  4600  0nelrel  4650  eqrelrdv  4700  xpsspw  4716  relint  4728  relop  4754  eqbrrdva  4774  opeldm  4807  elres  4920  relssres  4922  exse2  4978  issref  4986  trin2  4995  dminss  5018  imainss  5019  rnxpid  5038  dmsn0el  5073  dmmptg  5101  relrelss  5130  cnviinm  5145  iotanul  5168  sniota  5180  dffun5r  5200  funmo  5203  funco  5228  funun  5232  funprg  5238  funtpg  5239  funtp  5241  fntpg  5244  fununi  5256  funcnvuni  5257  imadiflem  5267  imainlem  5269  funimaexglem  5271  isarep2  5275  fnunsn  5295  2elresin  5299  fnimadisj  5308  dmmptd  5318  fco  5353  funssxp  5357  fssres  5363  feu  5370  fimacnvdisj  5372  fabexg  5375  f00  5379  f0rn0  5382  f1co  5405  fores  5419  foco  5420  f1ores  5447  foimacnv  5450  f1oun  5452  fun11iun  5453  f1oco  5455  fo00  5468  brprcneu  5479  fv3  5509  relelfvdm  5518  nfvres  5519  nfunsn  5520  funfvbrb  5598  respreima  5613  dff2  5629  dff3im  5630  dffo4  5633  fvmptelrn  5638  ffvresb  5648  f1oresrab  5650  fmptco  5651  fsn  5657  fpr  5667  ftpg  5669  fsnunf  5685  fsnunfv  5686  elabrex  5726  dff1o6  5744  foeqcnvco  5758  fliftel1  5762  isores1  5782  isoini2  5787  riotasbc  5813  acexmidlemph  5835  acexmidlemcase  5837  oprabidlem  5873  brabvv  5888  eloprabga  5929  fnoprabg  5943  caovimo  6035  oprabexd  6095  fo1stresm  6129  fo2ndresm  6130  unielxp  6142  1st2ndbr  6152  fmpoco  6184  1stconst  6189  2ndconst  6190  poxp  6200  spc2ed  6201  disjxp1  6204  reldmtpos  6221  tposfun  6228  dftpos4  6231  smores  6260  smores2  6262  tfrlem1  6276  tfr0dm  6290  tfrlemibxssdm  6295  tfrlemibex  6297  tfrlemiubacc  6298  tfrlemi14d  6301  tfrexlem  6302  tfri1d  6303  tfr1onlembxssdm  6311  tfr1onlembex  6313  tfr1onlemubacc  6314  tfr1onlemres  6317  tfrcllemsucfn  6321  tfrcllembxssdm  6324  tfrcllembex  6326  tfrcllemubacc  6327  tfrcllemres  6330  tfri3  6335  rdgon  6354  frecabcl  6367  frecfcllem  6372  frecrdg  6376  2oconcl  6407  nnsucelsuc  6459  nntri3or  6461  nndceq  6467  nndcel  6468  dcdifsnid  6472  ecexr  6506  brdifun  6528  ecelqsdm  6571  iinerm  6573  eroveu  6592  erovlem  6593  ecopovtrn  6598  ecopovtrng  6601  th3qlem1  6603  pmsspw  6649  map0b  6653  mapsn  6656  mapsncnv  6661  ixpf  6686  uniixp  6687  ixpexgg  6688  resixp  6699  f1oen3g  6720  ssdomg  6744  domtr  6751  snfig  6780  enpr2d  6783  xpf1o  6810  xpmapenlem  6815  php5dom  6829  fidceq  6835  nnfi  6838  fiunsnnn  6847  findcard  6854  findcard2  6855  findcard2s  6856  ac6sfi  6864  tridc  6865  fimax2gtri  6867  finexdc  6868  exmidpw  6874  exmidpweq  6875  nnwetri  6881  unsnfi  6884  unsnfidcex  6885  unsnfidcel  6886  undifdcss  6888  tpfidisj  6893  iunfidisj  6911  snexxph  6915  fidcenumlemrks  6918  sbthlem2  6923  sbthlemi3  6924  sbthlem7  6928  sbthlemi8  6929  fival  6935  dcfi  6946  supmoti  6958  djuss  7035  updjudhf  7044  updjud  7047  casefun  7050  caseinj  7054  omp1eomlem  7059  djufun  7069  djuinj  7071  ctssdccl  7076  ctfoex  7083  nnnninf  7090  nnnninfeq2  7093  nninfisollem0  7094  nninfisollemne  7095  nninfisollemeq  7096  nninfisol  7097  finomni  7104  exmidomniim  7105  exmidomni  7106  fodjuomnilemdc  7108  omniwomnimkv  7131  exmidonfinlem  7149  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  exmidaclem  7164  dju1en  7169  exmidontriimlem1  7177  exmidontriimlem3  7179  pw1on  7182  3nsssucpw1  7192  cc4f  7210  cc4n  7212  dmaddpqlem  7318  nqpi  7319  dmaddpq  7320  dmmulpq  7321  ltdcnq  7338  subhalfnqq  7355  enq0sym  7373  enq0ref  7374  enq0tr  7375  nqnq0pi  7379  nq0nn  7383  addnq0mo  7388  mulnq0mo  7389  nqpnq0nq  7394  nqnq0a  7395  nqnq0m  7396  npsspw  7412  elnp1st2nd  7417  prnmaxl  7429  prnminu  7430  prarloc  7444  genprndl  7462  genprndu  7463  nqprm  7483  nqprl  7492  nqpru  7493  addnqprlemrl  7498  addnqprlemru  7499  prmuloc  7507  mulnqprlemrl  7514  mulnqprlemru  7515  ltsopr  7537  ltexprlemm  7541  ltexprlemopl  7542  ltexprlemopu  7544  lteupri  7558  recexprlemopl  7566  recexprlemopu  7568  recexprlemdisj  7571  archpr  7584  cauappcvgprlemdisj  7592  cauappcvgprlemladdrl  7598  cauappcvgprlem2  7601  caucvgprlemnbj  7608  caucvgprlemdisj  7615  caucvgprlemladdfu  7618  caucvgprlem2  7621  caucvgprprlemnbj  7634  caucvgprprlemdisj  7643  suplocexprlemml  7657  suplocexprlemrl  7658  suplocexprlemmu  7659  suplocexprlemloc  7662  addsrmo  7684  mulsrmo  7685  recexgt0sr  7714  prsrpos  7726  caucvgsrlemasr  7731  suplocsrlemb  7747  suplocsrlempr  7748  suplocsr  7750  elrealeu  7770  pitonn  7789  pitoregt0  7790  pitore  7791  recnnre  7792  axaddcl  7805  axaddrcl  7806  axmulcl  7807  axmulrcl  7808  axrnegex  7820  axcnre  7822  axpre-lttrn  7825  rereceu  7830  axarch  7832  axpre-suploclemres  7842  axpre-suploc  7843  ltxrlt  7964  apirr  8503  divmulasscomap  8592  rerecclap  8626  lbreu  8840  arch  9111  0mnnnnn0  9146  nnm1nn0  9155  elnnnn0c  9159  elnnz1  9214  ztri3or0  9233  nzadd  9243  nn0n0n1ge2  9261  zdceq  9266  zdcle  9267  zdclt  9268  uzind  9302  eluzge3nn  9510  supinfneg  9533  infsupneg  9534  eluz2b2  9541  elnn1uz2  9545  elnn0dc  9549  elnndc  9550  nn01to3  9555  znq  9562  qaddcl  9573  qmulcl  9575  qreccl  9580  irradd  9584  irrmul  9585  elpq  9586  cnref1o  9588  xnn0dcle  9738  xrpnfdc  9778  xrmnfdc  9779  xaddcom  9797  xnegdi  9804  xpncan  9807  xleadd1a  9809  iooidg  9845  elioo4g  9870  fzdcel  9975  fznlem  9976  fzpreddisj  10006  fz0to4untppr  10059  elfz0ubfz0  10060  elfz0fzfz0  10061  fz0fzelfz0  10062  fz0fzdiffz0  10065  elfzmlbp  10067  difelfzle  10069  4fvwrd4  10075  fzosplit  10112  elfzo0  10117  fzo1fzo0n0  10118  elfzonn0  10121  fzofzim  10123  elfzo1  10125  elfzom1elp1fzo  10137  fzossfzop1  10147  ssfzo12bi  10160  exfzdc  10175  qdceq  10182  exbtwnzlemstep  10183  exbtwnzlemex  10185  exbtwnz  10186  rebtwn2zlemstep  10188  rebtwn2z  10190  qbtwnxr  10193  modfzo0difsn  10330  frec2uzrand  10340  frec2uzf1od  10341  frecuzrdgrcl  10345  frecuzrdgtcl  10347  frecuzrdgrclt  10350  frecuzrdgfunlem  10354  frecfzennn  10361  seq3f1olemp  10437  seq3f1oleml  10438  ser0f  10450  expcl2lemap  10467  hashunsng  10720  shftfvalg  10760  shftfval  10763  caucvgre  10923  rexanuz  10930  recvguniq  10937  rennim  10944  resqrexlemf  10949  rsqrmo  10969  fimaxre2  11168  climeu  11237  sumdc  11299  summodc  11324  zsumdc  11325  isum  11326  fisumss  11333  isumss2  11334  fsumsplit  11348  sumsnf  11350  fsumsplitsn  11351  sumtp  11355  sumsplitdc  11373  fsum2dlemstep  11375  fisum0diag2  11388  fsumconst  11395  modfsummodlemstep  11398  fsum00  11403  fsumabs  11406  fsumiun  11418  isumlessdc  11437  expcnv  11445  prodmodc  11519  zproddc  11520  iprodap  11521  iprodap0  11523  fprodssdc  11531  prodsnf  11533  fprodsplitdc  11537  fprodsplit  11538  fprodm1  11539  fprod1p  11540  fprodunsn  11545  fprod2dlemstep  11563  fprodsplitsn  11574  ef0lem  11601  modmulconst  11763  dvdsdivcl  11788  dvdsssfz1  11790  dvdsfac  11798  zeoxor  11806  nn0ehalf  11840  nn0oddm1d2  11846  nnoddm1d2  11847  divalglemeunn  11858  divalglemeuneg  11860  zsupcllemstep  11878  infssuzex  11882  gcdsupex  11890  gcdsupcl  11891  bezoutlemnewy  11929  bezoutlemmain  11931  bezoutlemeu  11940  dfgcd2  11947  nnwosdc  11972  algrf  11977  algcvgblem  11981  lcmgcdlem  12009  lcmdvds  12011  coprmgcdb  12020  mulgcddvds  12026  qredeu  12029  cncongr1  12035  cncongr2  12036  isprm2lem  12048  dvdsnprmd  12057  prmdc  12062  oddprmge3  12067  pw2dvdseu  12100  phibndlem  12148  dfphi2  12152  hashdvds  12153  phiprmpw  12154  eulerthlemh  12163  hashgcdeq  12171  phisum  12172  odzdvds  12177  reumodprminv  12185  nnnn0modprm0  12187  prm23ge5  12196  pclemdc  12220  pcdvdsb  12251  difsqpwdvds  12269  oddprmdvds  12284  1arith  12297  4sqlem3  12320  ennnfonelemdc  12332  ennnfonelemh  12337  ennnfonelemhf1o  12346  ennnfonelemf1  12351  ennnfonelemrn  12352  ennnfonelemdm  12353  exmidunben  12359  ctinfomlemom  12360  ctinfom  12361  ctiunctlemudc  12370  ctiunctlemf  12371  ctiunctal  12374  nninfdclemcl  12381  nninfdclemf  12382  nninfdclemp1  12383  isstructim  12408  setsresg  12432  strleund  12483  1strbas  12494  2strbasg  12496  2stropg  12497  restsspw  12566  mgmidsssn0  12615  istopon  12651  toponcom  12665  topgele  12667  topontopn  12675  tsettps  12676  tgval  12689  eltg2b  12694  unitg  12702  tgss2  12719  bastop2  12724  distop  12725  epttop  12730  cldss2  12746  neisspw  12788  neipsm  12794  neiuni  12801  tgcn  12848  tgcnp  12849  cnntr  12865  lmff  12889  txuni2  12896  txbasex  12897  txbas  12898  txcnp  12911  txcnmpt  12913  txcn  12915  txdis  12917  txdis1cn  12918  cnmpt11  12923  cnmpt12  12927  cnmpt21  12931  cnmpt2t  12933  cnmpt22  12934  blsscls2  13133  xmetxpbl  13148  xmettxlem  13149  tgqioo  13187  fsumcncntop  13196  cncfmpt1f  13224  mulcncflem  13230  mulcncf  13231  dedekindeu  13241  dedekindicclemicc  13250  dedekindicc  13251  ivthinclemdisj  13258  limcimo  13274  cnmptlimc  13283  reldvg  13288  dvfvalap  13290  dvfgg  13297  dveflem  13327  dvef  13328  sincn  13330  coscn  13331  reeff1o  13334  pilem3  13344  ioocosf1o  13415  lgsne0  13579  2sqlem2  13591  mul2sq  13592  2sqlem3  13593  2sqlem7  13597  bj-trst  13620  bj-fast  13622  bj-stand  13629  bj-trdc  13633  bj-fadc  13635  decidr  13677  djulclALT  13682  djurclALT  13683  bj-charfunr  13692  bj-indind  13814  bj-2inf  13820  bj-nntrans2  13834  bj-peano4  13837  bj-nnord  13840  bj-inf2vn  13856  bj-inf2vn2  13857  bj-findis  13861  pwf1oexmid  13879  exmid1stab  13880  subctctexmid  13881  nnsf  13885  nninfsellemdc  13890  nninffeq  13900  exmidsbthrlem  13901  sbthom  13905  triap  13908  trilpo  13922  apdifflemr  13926  redcwlpo  13934  tridceq  13935  nconstwlpolem0  13941  nconstwlpolem  13943  nconstwlpo  13944  neapmkv  13946