ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylibr Unicode version

Theorem sylibr 141
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
StepHypRef Expression
1 sylibr.1 . 2  |-  ( ph  ->  ps )
2 sylibr.2 . . 3  |-  ( ch  <->  ps )
32biimpri 128 . 2  |-  ( ps 
->  ch )
41, 3syl 14 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  pm5.74rd  176  bitri  177  3imtr4i  194  sylanbrc  402  dcimpstab  763  dcim  795  oibabs  811  stabtestimpdc  835  dcor  854  3mix1  1084  3mix2  1085  3jca  1095  syl3anbrc  1099  inegd  1279  pclem6  1281  xoranor  1284  nfxfrd  1380  nfd  1432  hban  1455  nfan1  1472  nford  1475  nfand  1476  hbim1  1478  alexim  1552  ax6blem  1556  nf4r  1577  19.34  1590  nfexd  1660  sbcof2  1707  nfsb2or  1734  sbidm  1747  nfdv  1773  nfeudv  1931  mon  1945  eumo  1948  mo23  1957  eu2  1960  eu3h  1961  exmodc  1966  exmonim  1967  mo2r  1968  mo3h  1969  bm1.1  2041  eqrdv  2054  3eltr4g  2139  abbi2dv  2172  abbi1dv  2173  nfcd  2189  nfcxfrd  2192  dcned  2226  neqned  2227  3netr4g  2255  necon3bi  2270  necon2ai  2274  alral  2384  rspe  2387  rsp2e  2389  rgen2a  2392  ralrimi  2407  r19.27av  2465  r19.32r  2474  nfreudxy  2500  mormo  2538  nrexrmo  2543  cgsex2g  2607  cgsex4g  2608  spc2egv  2659  spc2gv  2660  spc3egv  2661  spc3gv  2662  rspce  2668  ceqex  2694  elrab3t  2720  mosubt  2741  mo2icl  2743  reu3  2754  reu6i  2755  2rmorex  2768  sbc5  2810  rspesbca  2870  rmo2ilem  2875  sbnfc2  2934  ssrd  2978  ssrdv  2979  3sstr4g  3014  syl5eqss  3017  ss2abdv  3041  abssdv  3042  rabssdv  3048  ss2rabdv  3049  ssun1  3134  unssad  3148  unssbd  3149  ssddif  3199  uneqin  3216  indifdir  3221  undif3ss  3226  reuss2  3245  n0rf  3261  reximdva0m  3264  rabxmdc  3277  ssindif0im  3309  minel  3311  ralidm  3349  ralm  3353  disjsn2  3461  absneu  3470  rabsneu  3471  opprc  3598  elunii  3613  dfnfc2  3626  uniss2  3639  unidif  3640  ssunieq  3641  intab  3672  iunss2  3730  iunxdif2  3733  invdisj  3787  3brtr4g  3824  trin  3892  triun  3895  truni  3896  trint  3897  iinexgm  3936  class2seteq  3944  pwuni  3971  mss  3990  copsex2t  4010  euotd  4019  pwunim  4051  ispod  4069  sotricim  4088  exse  4101  frind  4117  trssord  4145  suctr  4186  eusvnf  4213  eusvnfb  4214  eusv2nf  4216  rexxfrd  4223  ralxfr2d  4224  rexxfr2d  4225  rabxfrd  4229  reuhypd  4231  eldifpw  4236  iunpw  4239  ssorduni  4241  sucelon  4257  onsucelsucr  4262  sucunielr  4264  ordtri2or2exmidlem  4279  onsucelsucexmid  4283  reg2exmidlema  4287  setindel  4291  elirr  4294  orddisj  4298  en2lp  4306  suc11g  4309  ordsuc  4315  nlimsucg  4318  onpsssuc  4323  ordtri2or2exmid  4324  zfregfr  4326  wessep  4330  tfi  4333  peano5  4349  limom  4364  peano2b  4365  nndceq0  4367  eqrelrdv  4464  xpsspw  4478  relint  4489  relop  4514  eqbrrdva  4533  opeldm  4566  elres  4674  relssres  4676  exse2  4727  issref  4735  trin2  4744  dminss  4766  imainss  4767  rnxpid  4783  dmsn0el  4818  dmmptg  4846  relrelss  4872  cnviinm  4887  iotanul  4910  sniota  4922  dffun5r  4942  funmo  4945  funco  4968  funun  4972  funprg  4977  funtpg  4978  funtp  4980  fntpg  4983  fununi  4995  funcnvuni  4996  imadiflem  5006  imainlem  5008  funimaexglem  5010  isarep2  5014  fnunsn  5034  2elresin  5038  fnimadisj  5047  fco  5084  funssxp  5088  fssres  5094  feu  5100  fimacnvdisj  5102  fabexg  5105  f00  5109  f1co  5129  fores  5143  foco  5144  f1ores  5169  foimacnv  5172  f1oun  5174  fun11iun  5175  f1oco  5177  fo00  5190  brprcneu  5199  fv3  5225  relelfvdm  5233  nfvres  5234  nfunsn  5235  funfvbrb  5308  respreima  5323  dff2  5339  dff3im  5340  dffo4  5343  ffvresb  5356  f1oresrab  5357  fmptco  5358  fsn  5363  fpr  5373  ftpg  5375  fsnunf  5390  fsnunfv  5391  elabrex  5425  dff1o6  5444  foeqcnvco  5458  fliftel1  5462  isores1  5482  isoini2  5486  riotasbc  5511  acexmidlemph  5533  acexmidlemcase  5535  oprabidlem  5564  brabvv  5579  eloprabga  5619  fnoprabg  5630  caovimo  5722  oprabexd  5782  fo1stresm  5816  fo2ndresm  5817  unielxp  5828  1st2ndbr  5838  fmpt2co  5865  1stconst  5870  2ndconst  5871  poxp  5881  spc2ed  5882  reldmtpos  5899  tposfun  5906  dftpos4  5909  smores  5938  smores2  5940  tfrlem1  5954  tfr0  5968  tfrlemibxssdm  5972  tfrlemibex  5974  tfrlemiubacc  5975  tfrlemi14d  5978  tfrexlem  5979  tfri1d  5980  tfri3  5984  2oconcl  6053  nnsucelsuc  6101  nntri3or  6103  nndceq  6108  nndcel  6109  nndifsnid  6111  ecexr  6142  brdifun  6164  ecelqsdm  6207  iinerm  6209  eroveu  6228  erovlem  6229  ecopovtrn  6234  ecopovtrng  6237  th3qlem1  6239  f1oen3g  6265  ssdomg  6289  domtr  6296  snfig  6322  php5dom  6356  fidceq  6361  fidifsnid  6363  nnfi  6364  fiunsnnn  6369  findcard  6376  findcard2  6377  findcard2s  6378  ac6sfi  6383  nnwetri  6385  supmoti  6399  dmaddpqlem  6533  nqpi  6534  dmaddpq  6535  dmmulpq  6536  ltdcnq  6553  subhalfnqq  6570  enq0sym  6588  enq0ref  6589  enq0tr  6590  nqnq0pi  6594  nq0nn  6598  addnq0mo  6603  mulnq0mo  6604  nqpnq0nq  6609  nqnq0a  6610  nqnq0m  6611  npsspw  6627  elnp1st2nd  6632  prnmaxl  6644  prnminu  6645  prarloc  6659  genprndl  6677  genprndu  6678  nqprm  6698  nqprl  6707  nqpru  6708  addnqprlemrl  6713  addnqprlemru  6714  prmuloc  6722  mulnqprlemrl  6729  mulnqprlemru  6730  ltsopr  6752  ltexprlemm  6756  ltexprlemopl  6757  ltexprlemopu  6759  lteupri  6773  recexprlemopl  6781  recexprlemopu  6783  recexprlemdisj  6786  archpr  6799  cauappcvgprlemdisj  6807  cauappcvgprlemladdrl  6813  cauappcvgprlem2  6816  caucvgprlemnbj  6823  caucvgprlemdisj  6830  caucvgprlemladdfu  6833  caucvgprlem2  6836  caucvgprprlemnbj  6849  caucvgprprlemdisj  6858  addsrmo  6886  mulsrmo  6887  recexgt0sr  6916  prsrpos  6927  caucvgsrlemasr  6932  elrealeu  6964  pitonn  6982  pitoregt0  6983  pitore  6984  recnnre  6985  axaddcl  6998  axaddrcl  6999  axmulcl  7000  axmulrcl  7001  axrnegex  7011  axcnre  7013  axpre-lttrn  7016  rereceu  7021  axarch  7023  ltxrlt  7144  apirr  7670  rerecclap  7781  arch  8236  0mnnnnn0  8271  nnm1nn0  8280  elnnnn0c  8284  elnnz1  8325  ztri3or0  8344  nzadd  8354  nn0n0n1ge2  8369  zdceq  8374  zdcle  8375  zdclt  8376  uzind  8408  eluzge3nn  8610  eluz2b2  8637  elnn1uz2  8641  nn01to3  8649  znq  8656  qaddcl  8667  qmulcl  8669  qreccl  8674  irradd  8678  irrmul  8679  cnref1o  8680  iooidg  8879  elioo4g  8904  fzdcel  9006  fznlem  9007  fzpreddisj  9035  elfz0ubfz0  9084  elfz0fzfz0  9085  fz0fzelfz0  9086  fz0fzdiffz0  9089  elfzmlbp  9092  difelfzle  9094  4fvwrd4  9099  fzosplit  9135  elfzo0  9140  fzo1fzo0n0  9141  elfzonn0  9144  fzofzim  9146  elfzo1  9148  elfzom1elp1fzo  9160  fzossfzop1  9170  ssfzo12bi  9183  qdceq  9204  qbtwnzlemstep  9205  qbtwnzlemex  9207  qbtwnz  9208  rebtwn2zlemstep  9209  rebtwn2z  9211  qbtwnxr  9214  modfzo0difsn  9345  frec2uzrand  9355  frec2uzf1od  9356  frecuzrdgrom  9360  frecuzrdgfn  9362  frecfzennn  9367  iseqf  9388  iser0f  9416  expcl2lemap  9432  shftfvalg  9647  shftfval  9650  caucvgre  9808  rexanuz  9815  recvguniq  9822  rennim  9829  resqrexlemf  9834  rsqrmo  9854  climeu  10048  modmulconst  10139  dvdsdivcl  10162  dvdsssfz1  10164  dvdsfac  10172  zeoxor  10180  nn0ehalf  10215  nn0oddm1d2  10221  nnoddm1d2  10222  divalglemeunn  10233  divalglemeuneg  10235  pw2dvdseu  10256  ialgrf  10267  algcvgblem  10271  bj-nfalt  10291  bj-indind  10443  bj-2inf  10449  peano5setOLD  10452  bj-nntrans2  10464  bj-peano4  10467  bj-nnord  10470  bj-inf2vn  10486  bj-inf2vn2  10487  bj-findis  10491
  Copyright terms: Public domain W3C validator