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-1 5  ax-2 6  ax-mp 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  411  oibabs  686  dcim  809  dcstab  812  stdcndc  813  stdcndcOLD  814  dcor  900  3mix1  1131  3mix2  1132  3jca  1142  syl3anbrc  1146  inegd  1331  pclem6  1333  xoranor  1336  nfxfrd  1432  nfd  1484  hban  1507  nfan1  1524  nford  1527  nfand  1528  hbim1  1530  alexim  1605  ax6blem  1609  nf4r  1630  19.34  1643  nfexd  1715  sbcof2  1762  nfsb2or  1789  sbidm  1803  nfdv  1829  nfeudv  1988  mon  2002  eumo  2005  mo23  2014  eu2  2017  eu3h  2018  exmodc  2023  exmonim  2024  mo2r  2025  mo3h  2026  bm1.1  2098  eqrdv  2111  3eltr4g  2198  abbi2dv  2231  abbi1dv  2232  nfcd  2248  nfcxfrd  2251  dcned  2286  neqned  2287  3netr4g  2315  necon3bi  2330  necon2ai  2334  alral  2450  rspe  2453  rsp2e  2455  rgen2a  2458  ralrimi  2475  r19.27v  2531  r19.28v  2532  r19.27av  2539  r19.32r  2550  nfreudxy  2576  mormo  2614  nrexrmo  2619  cgsex2g  2691  cgsex4g  2692  spc2egv  2744  spc2gv  2745  spc3egv  2746  spc3gv  2747  rspce  2753  ceqex  2780  elrab3t  2806  elrabd  2809  mosubt  2828  mo2icl  2830  reu3  2841  reu6i  2842  2rmorex  2857  sbc5  2899  rspesbca  2959  rmo2ilem  2964  sbnfc2  3024  ssrd  3066  ssrdv  3067  3sstr4g  3104  syl5eqss  3107  ss2abdv  3134  abssdv  3135  rabssdv  3141  ss2rabdv  3142  ssun1  3203  unssad  3217  unssbd  3218  ssddif  3274  uneqin  3291  indifdir  3296  undif3ss  3301  reuss2  3320  n0rf  3339  reximdva0m  3342  rabxmdc  3358  ssindif0im  3386  minel  3388  ralidm  3427  ralm  3431  dcun  3437  ifmdc  3473  disjsn2  3550  absneu  3559  rabsneu  3560  opprc  3690  elunii  3705  dfnfc2  3718  uniss2  3731  unidif  3732  ssunieq  3733  intab  3764  iunss2  3822  iunxdif2  3825  invdisj  3887  disjiun  3888  3brtr4g  3925  trin  3994  triun  3997  truni  3998  trint  3999  iinexgm  4037  class2seteq  4045  pwuni  4074  exmid1dc  4081  exmidn0m  4082  exmidsssn  4083  exmid0el  4085  exmidel  4086  exmidundif  4087  exmidundifim  4088  mss  4106  copsex2t  4125  euotd  4134  pwunim  4166  ispod  4184  sotricim  4203  exse  4216  frind  4232  trssord  4260  suctr  4301  pwnex  4328  eusvnf  4332  eusvnfb  4333  eusv2nf  4335  rexxfrd  4342  ralxfr2d  4343  rexxfr2d  4344  rabxfrd  4348  reuhypd  4350  eldifpw  4356  iunpw  4359  ssorduni  4361  sucelon  4377  onsucelsucr  4382  sucunielr  4384  ordtri2or2exmidlem  4399  onsucelsucexmid  4403  reg2exmidlema  4407  setindel  4411  elirr  4414  orddisj  4419  en2lp  4427  suc11g  4430  ordsuc  4436  nlimsucg  4439  ordtri2or2exmid  4444  zfregfr  4446  wessep  4450  tfi  4454  peano5  4470  limom  4485  peano2b  4486  nndceq0  4489  nnpredcl  4494  0nelrel  4543  eqrelrdv  4593  xpsspw  4609  relint  4621  relop  4647  eqbrrdva  4667  opeldm  4700  elres  4811  relssres  4813  exse2  4869  issref  4877  trin2  4886  dminss  4909  imainss  4910  rnxpid  4929  dmsn0el  4964  dmmptg  4992  relrelss  5021  cnviinm  5036  iotanul  5059  sniota  5071  dffun5r  5091  funmo  5094  funco  5119  funun  5123  funprg  5129  funtpg  5130  funtp  5132  fntpg  5135  fununi  5147  funcnvuni  5148  imadiflem  5158  imainlem  5160  funimaexglem  5162  isarep2  5166  fnunsn  5186  2elresin  5190  fnimadisj  5199  dmmptd  5209  fco  5244  funssxp  5248  fssres  5254  feu  5261  fimacnvdisj  5263  fabexg  5266  f00  5270  f0rn0  5273  f1co  5296  fores  5310  foco  5311  f1ores  5336  foimacnv  5339  f1oun  5341  fun11iun  5342  f1oco  5344  fo00  5357  brprcneu  5366  fv3  5396  relelfvdm  5405  nfvres  5406  nfunsn  5407  funfvbrb  5485  respreima  5500  dff2  5516  dff3im  5517  dffo4  5520  fvmptelrn  5525  ffvresb  5535  f1oresrab  5537  fmptco  5538  fsn  5544  fpr  5554  ftpg  5556  fsnunf  5572  fsnunfv  5573  elabrex  5611  dff1o6  5629  foeqcnvco  5643  fliftel1  5647  isores1  5667  isoini2  5672  riotasbc  5697  acexmidlemph  5719  acexmidlemcase  5721  oprabidlem  5754  brabvv  5769  eloprabga  5810  fnoprabg  5824  caovimo  5916  oprabexd  5976  fo1stresm  6010  fo2ndresm  6011  unielxp  6023  1st2ndbr  6033  fmpoco  6064  1stconst  6069  2ndconst  6070  poxp  6080  spc2ed  6081  disjxp1  6084  reldmtpos  6101  tposfun  6108  dftpos4  6111  smores  6140  smores2  6142  tfrlem1  6156  tfr0dm  6170  tfrlemibxssdm  6175  tfrlemibex  6177  tfrlemiubacc  6178  tfrlemi14d  6181  tfrexlem  6182  tfri1d  6183  tfr1onlembxssdm  6191  tfr1onlembex  6193  tfr1onlemubacc  6194  tfr1onlemres  6197  tfrcllemsucfn  6201  tfrcllembxssdm  6204  tfrcllembex  6206  tfrcllemubacc  6207  tfrcllemres  6210  tfri3  6215  rdgon  6234  frecabcl  6247  frecfcllem  6252  frecrdg  6256  2oconcl  6287  nnsucelsuc  6338  nntri3or  6340  nndceq  6346  nndcel  6347  dcdifsnid  6351  ecexr  6385  brdifun  6407  ecelqsdm  6450  iinerm  6452  eroveu  6471  erovlem  6472  ecopovtrn  6477  ecopovtrng  6480  th3qlem1  6482  pmsspw  6528  map0b  6532  mapsn  6535  mapsncnv  6540  ixpf  6565  uniixp  6566  ixpexgg  6567  resixp  6578  f1oen3g  6599  ssdomg  6623  domtr  6630  snfig  6659  xpf1o  6688  xpmapenlem  6693  php5dom  6707  fidceq  6713  nnfi  6716  fiunsnnn  6725  findcard  6732  findcard2  6733  findcard2s  6734  ac6sfi  6742  tridc  6743  fimax2gtri  6745  finexdc  6746  exmidpw  6752  nnwetri  6754  unsnfi  6757  unsnfidcex  6758  unsnfidcel  6759  undifdcss  6761  tpfidisj  6766  iunfidisj  6783  snexxph  6787  fidcenumlemrks  6790  sbthlem2  6795  sbthlemi3  6796  sbthlem7  6800  sbthlemi8  6801  fival  6807  supmoti  6829  djuss  6904  updjudhf  6913  updjud  6916  casefun  6919  caseinj  6923  omp1eomlem  6928  djufun  6938  djuinj  6940  ctssdccl  6945  finomni  6959  exmidomniim  6960  exmidomni  6961  fodjuomnilemdc  6963  nnnninf  6970  exmidfodomrlemr  7002  exmidfodomrlemrALT  7003  exmidaclem  7008  dju1en  7013  dmaddpqlem  7126  nqpi  7127  dmaddpq  7128  dmmulpq  7129  ltdcnq  7146  subhalfnqq  7163  enq0sym  7181  enq0ref  7182  enq0tr  7183  nqnq0pi  7187  nq0nn  7191  addnq0mo  7196  mulnq0mo  7197  nqpnq0nq  7202  nqnq0a  7203  nqnq0m  7204  npsspw  7220  elnp1st2nd  7225  prnmaxl  7237  prnminu  7238  prarloc  7252  genprndl  7270  genprndu  7271  nqprm  7291  nqprl  7300  nqpru  7301  addnqprlemrl  7306  addnqprlemru  7307  prmuloc  7315  mulnqprlemrl  7322  mulnqprlemru  7323  ltsopr  7345  ltexprlemm  7349  ltexprlemopl  7350  ltexprlemopu  7352  lteupri  7366  recexprlemopl  7374  recexprlemopu  7376  recexprlemdisj  7379  archpr  7392  cauappcvgprlemdisj  7400  cauappcvgprlemladdrl  7406  cauappcvgprlem2  7409  caucvgprlemnbj  7416  caucvgprlemdisj  7423  caucvgprlemladdfu  7426  caucvgprlem2  7429  caucvgprprlemnbj  7442  caucvgprprlemdisj  7451  addsrmo  7479  mulsrmo  7480  recexgt0sr  7509  prsrpos  7520  caucvgsrlemasr  7525  elrealeu  7557  pitonn  7576  pitoregt0  7577  pitore  7578  recnnre  7579  axaddcl  7592  axaddrcl  7593  axmulcl  7594  axmulrcl  7595  axrnegex  7607  axcnre  7609  axpre-lttrn  7612  rereceu  7617  axarch  7619  ltxrlt  7747  apirr  8278  cnstab  8317  divmulasscomap  8362  rerecclap  8396  lbreu  8606  arch  8871  0mnnnnn0  8906  nnm1nn0  8915  elnnnn0c  8919  elnnz1  8974  ztri3or0  8993  nzadd  9003  nn0n0n1ge2  9018  zdceq  9023  zdcle  9024  zdclt  9025  uzind  9059  eluzge3nn  9262  supinfneg  9285  infsupneg  9286  eluz2b2  9292  elnn1uz2  9296  nn01to3  9304  znq  9311  qaddcl  9322  qmulcl  9324  qreccl  9329  irradd  9333  irrmul  9334  cnref1o  9335  xrpnfdc  9511  xrmnfdc  9512  xaddcom  9530  xnegdi  9537  xpncan  9540  xleadd1a  9542  iooidg  9578  elioo4g  9603  fzdcel  9706  fznlem  9707  fzpreddisj  9737  elfz0ubfz0  9788  elfz0fzfz0  9789  fz0fzelfz0  9790  fz0fzdiffz0  9793  elfzmlbp  9795  difelfzle  9797  4fvwrd4  9803  fzosplit  9840  elfzo0  9845  fzo1fzo0n0  9846  elfzonn0  9849  fzofzim  9851  elfzo1  9853  elfzom1elp1fzo  9865  fzossfzop1  9875  ssfzo12bi  9888  exfzdc  9903  qdceq  9910  exbtwnzlemstep  9911  exbtwnzlemex  9913  exbtwnz  9914  rebtwn2zlemstep  9916  rebtwn2z  9918  qbtwnxr  9921  modfzo0difsn  10054  frec2uzrand  10064  frec2uzf1od  10065  frecuzrdgrcl  10069  frecuzrdgtcl  10071  frecuzrdgrclt  10074  frecuzrdgfunlem  10078  frecfzennn  10085  seq3f1olemp  10161  seq3f1oleml  10162  ser0f  10174  expcl2lemap  10191  hashunsng  10439  shftfvalg  10476  shftfval  10479  caucvgre  10638  rexanuz  10645  recvguniq  10652  rennim  10659  resqrexlemf  10664  rsqrmo  10684  fimaxre2  10883  climeu  10950  sumdc  11012  summodc  11037  zsumdc  11038  isum  11039  fisumss  11046  isumss2  11047  fsumsplit  11061  sumsnf  11063  fsumsplitsn  11064  sumtp  11068  sumsplitdc  11086  fsum2dlemstep  11088  fisum0diag2  11101  fsumconst  11108  modfsummodlemstep  11111  fsum00  11116  fsumabs  11119  fsumiun  11131  isumlessdc  11150  expcnv  11158  ef0lem  11210  modmulconst  11366  dvdsdivcl  11389  dvdsssfz1  11391  dvdsfac  11399  zeoxor  11407  nn0ehalf  11441  nn0oddm1d2  11447  nnoddm1d2  11448  divalglemeunn  11459  divalglemeuneg  11461  zsupcllemstep  11479  infssuzex  11483  gcdsupex  11487  gcdsupcl  11488  bezoutlemnewy  11523  bezoutlemmain  11525  bezoutlemeu  11534  dfgcd2  11541  algrf  11565  algcvgblem  11569  lcmgcdlem  11597  lcmdvds  11599  coprmgcdb  11608  mulgcddvds  11614  qredeu  11617  cncongr1  11623  cncongr2  11624  isprm2lem  11636  dvdsnprmd  11645  oddprmge3  11654  pw2dvdseu  11684  phibndlem  11730  dfphi2  11734  hashdvds  11735  phiprmpw  11736  hashgcdeq  11742  ennnfonelemdc  11750  ennnfonelemh  11755  ennnfonelemhf1o  11764  ennnfonelemf1  11769  ennnfonelemrn  11770  ennnfonelemdm  11771  exmidunben  11777  ctinfomlemom  11778  ctinfom  11779  ctiunctlemudc  11786  ctiunctlemf  11787  isstructim  11809  setsresg  11833  strleund  11883  1strbas  11894  2strbasg  11896  2stropg  11897  restsspw  11966  istopon  12016  toponcom  12030  topgele  12032  topontopn  12040  tsettps  12041  tgval  12054  eltg2b  12059  unitg  12067  tgss2  12084  bastop2  12089  distop  12090  epttop  12095  cldss2  12111  neisspw  12153  neipsm  12159  neiuni  12166  tgcn  12212  tgcnp  12213  cnntr  12229  lmff  12253  txuni2  12260  txbasex  12261  txbas  12262  txcnp  12275  txcnmpt  12277  txcn  12279  txdis  12281  txdis1cn  12282  cnmpt11  12287  cnmpt12  12291  cnmpt21  12295  cnmpt2t  12297  cnmpt22  12298  blsscls2  12475  xmetxpbl  12490  xmettxlem  12491  tgqioo  12526  fsumcncntop  12535  cncfmpt1f  12563  mulcncflem  12569  mulcncf  12570  limcimo  12583  cnmptlimc  12592  reldvg  12596  dvfvalap  12598  dvfgg  12605  bj-nnal  12629  bj-trst  12630  bj-fast  12631  bj-stand  12635  bj-trdc  12637  bj-fadc  12638  decidr  12682  djulclALT  12687  djurclALT  12688  bj-indind  12809  bj-2inf  12815  bj-nntrans2  12829  bj-peano4  12832  bj-nnord  12835  bj-inf2vn  12851  bj-inf2vn2  12852  bj-findis  12856  pwf1oexmid  12873  nnsf  12876  nninfsellemdc  12883  nninffeq  12893  exmidsbthrlem  12894  sbthom  12898  triap  12901  trilpo  12913