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

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
StepHypRef Expression
1 sylibr.1 . 2  |-  ( ph  ->  ps )
2 sylibr.2 . . 3  |-  ( ch  <->  ps )
32biimpri 133 . 2  |-  ( ps 
->  ch )
41, 3syl 14 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
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  715  dcim  842  dcstab  845  stdcndc  846  stdcndcOLD  847  dcand  934  dcor  937  3mix1  1168  3mix2  1169  3jca  1179  syl3anbrc  1183  syl21anbrc  1184  inegd  1383  pclem6  1385  xoranor  1388  nfxfrd  1486  nfd  1534  hban  1558  nfan1  1575  nford  1578  nfand  1579  hbim1  1581  nfal  1587  alexim  1656  nnal  1660  ax6blem  1661  nf4r  1682  19.34  1695  nfexd  1772  sbcof2  1821  nfsb2or  1848  sbidm  1862  nfdv  1888  nfd2  2034  nfeudv  2053  mon  2067  eumo  2070  mo23  2079  eu2  2082  eu3h  2083  exmodc  2088  exmonim  2089  mo2r  2090  mo3h  2091  bm1.1  2174  eqrdv  2187  3eltr4g  2275  abbi2dv  2308  abbi1dv  2309  nfcd  2327  nfcxfrd  2330  dcned  2366  neqned  2367  3netr4g  2395  necon3bi  2410  necon2ai  2414  nnral  2480  alral  2535  rspe  2539  rsp2e  2541  rgen2a  2544  ralrimi  2561  r19.27v  2617  r19.28v  2618  r19.27av  2625  r19.32r  2636  nfreudxy  2664  mormo  2702  nrexrmo  2707  cgsex2g  2788  cgsex4g  2789  spc2egv  2842  spc2gv  2843  spc3egv  2844  spc3gv  2845  rspce  2851  ceqex  2879  elrab3t  2907  elrabd  2910  mosubt  2929  mo2icl  2931  reu3  2942  reu6i  2943  2rmorex  2958  sbc5  3001  rspesbca  3062  rmo2ilem  3067  sbnfc2  3132  ssrd  3175  ssrdv  3176  3sstr4g  3213  eqsstrid  3216  ss2abdv  3243  abssdv  3244  rabssdv  3250  ss2rabdv  3251  ssun1  3313  unssad  3327  unssbd  3328  ssddif  3384  uneqin  3401  indifdir  3406  undif3ss  3411  reuss2  3430  n0rf  3450  reximdva0m  3453  rabxmdc  3469  ssindif0im  3497  minel  3499  ralidm  3538  ralm  3542  dcun  3548  ifmdc  3589  disjsn2  3670  absneu  3679  rabsneu  3680  opprc  3814  elunii  3829  dfnfc2  3842  uniss2  3855  unidif  3856  ssunieq  3857  intab  3888  iunss2  3946  iunssd  3947  iunxdif2  3950  invdisj  4012  disjiun  4013  3brtr4g  4052  trin  4126  triun  4129  truni  4130  trint  4131  iinexgm  4169  class2seteq  4178  pwuni  4207  exmid1dc  4215  exmidn0m  4216  exmidsssn  4217  exmid0el  4219  exmidel  4220  exmidundif  4221  exmidundifim  4222  exmid1stab  4223  mss  4241  copsex2t  4260  euotd  4269  pwunim  4301  ispod  4319  sotricim  4338  exse  4351  frind  4367  trssord  4395  suctr  4436  pwnex  4464  eusvnf  4468  eusvnfb  4469  eusv2nf  4471  rexxfrd  4478  ralxfr2d  4479  rexxfr2d  4480  rabxfrd  4484  reuhypd  4486  eldifpw  4492  iunpw  4495  ssorduni  4501  onsucb  4517  onsucelsucr  4522  sucunielr  4524  ontriexmidim  4536  ordtri2or2exmidlem  4540  onsucelsucexmid  4544  reg2exmidlema  4548  setindel  4552  elirr  4555  orddisj  4560  en2lp  4568  suc11g  4571  ordsuc  4577  nlimsucg  4580  ordtri2or2exmid  4585  ontri2orexmidim  4586  zfregfr  4588  wessep  4592  tfi  4596  peano5  4612  limom  4628  peano2b  4629  nndceq0  4632  nnpredcl  4637  0nelrel  4687  eqrelrdv  4737  xpsspw  4753  relint  4765  relop  4792  eqbrrdva  4812  opeldm  4845  elres  4958  relssres  4960  elrelimasn  5009  exse2  5017  issref  5026  trin2  5035  dminss  5058  imainss  5059  rnxpid  5078  dmsn0el  5113  dmmptg  5141  relrelss  5170  cnviinm  5185  iotanul  5208  sniota  5223  dffun5r  5244  funmo  5247  funco  5272  funun  5276  funprg  5282  funtpg  5283  funtp  5285  fntpg  5288  fununi  5300  funcnvuni  5301  imadiflem  5311  imainlem  5313  funimaexglem  5315  isarep2  5319  fnunsn  5339  2elresin  5343  fnimadisj  5352  dmmptd  5362  fco  5397  funssxp  5401  fssres  5407  feu  5414  fimacnvdisj  5416  fabexg  5419  f00  5423  f0rn0  5426  f1co  5449  fores  5463  foco  5464  f1ores  5492  foimacnv  5495  f1oun  5497  fun11iun  5498  f1oco  5500  fo00  5513  brprcneu  5524  fv3  5554  relelfvdm  5563  nfvres  5564  nfunsn  5565  funfvbrb  5646  respreima  5661  dff2  5677  dff3im  5678  dffo4  5681  fvmptelcdm  5686  ffvresb  5696  f1oresrab  5698  fmptco  5699  fsn  5705  fpr  5715  ftpg  5717  fsnunf  5733  fsnunfv  5734  elabrex  5775  dff1o6  5794  foeqcnvco  5808  fliftel1  5812  isores1  5832  isoini2  5837  riotasbc  5863  acexmidlemph  5885  acexmidlemcase  5887  oprabidlem  5923  brabvv  5938  eloprabga  5979  fnoprabg  5993  caovimo  6086  oprabexd  6147  fo1stresm  6181  fo2ndresm  6182  unielxp  6194  1st2ndbr  6204  fmpoco  6236  1stconst  6241  2ndconst  6242  poxp  6252  spc2ed  6253  disjxp1  6256  reldmtpos  6273  tposfun  6280  dftpos4  6283  smores  6312  smores2  6314  tfrlem1  6328  tfr0dm  6342  tfrlemibxssdm  6347  tfrlemibex  6349  tfrlemiubacc  6350  tfrlemi14d  6353  tfrexlem  6354  tfri1d  6355  tfr1onlembxssdm  6363  tfr1onlembex  6365  tfr1onlemubacc  6366  tfr1onlemres  6369  tfrcllemsucfn  6373  tfrcllembxssdm  6376  tfrcllembex  6378  tfrcllemubacc  6379  tfrcllemres  6382  tfri3  6387  rdgon  6406  frecabcl  6419  frecfcllem  6424  frecrdg  6428  2oconcl  6459  nnsucelsuc  6511  nntri3or  6513  nndceq  6519  nndcel  6520  dcdifsnid  6524  ecexr  6559  brdifun  6581  ecelqsdm  6626  iinerm  6628  eroveu  6647  erovlem  6648  ecopovtrn  6653  ecopovtrng  6656  th3qlem1  6658  pmsspw  6704  map0b  6708  mapsn  6711  mapsncnv  6716  ixpf  6741  uniixp  6742  ixpexgg  6743  resixp  6754  f1oen3g  6775  ssdomg  6799  domtr  6806  snfig  6835  enpr2d  6838  xpf1o  6867  xpmapenlem  6872  php5dom  6886  fidceq  6892  nnfi  6895  fiunsnnn  6904  findcard  6911  findcard2  6912  findcard2s  6913  ac6sfi  6921  tridc  6922  fimax2gtri  6924  finexdc  6925  exmidpw  6931  exmidpweq  6932  exmidpw2en  6935  nnwetri  6939  unsnfi  6942  unsnfidcex  6943  unsnfidcel  6944  undifdcss  6946  tpfidisj  6951  iunfidisj  6970  snexxph  6974  fidcenumlemrks  6977  sbthlem2  6982  sbthlemi3  6983  sbthlem7  6987  sbthlemi8  6988  fival  6994  dcfi  7005  supmoti  7017  djuss  7094  updjudhf  7103  updjud  7106  casefun  7109  caseinj  7113  omp1eomlem  7118  djufun  7128  djuinj  7130  ctssdccl  7135  ctfoex  7142  nnnninf  7149  nnnninfeq2  7152  nninfisollem0  7153  nninfisollemne  7154  nninfisollemeq  7155  nninfisol  7156  finomni  7163  exmidomniim  7164  exmidomni  7165  fodjuomnilemdc  7167  omniwomnimkv  7190  nninfdcinf  7194  nninfwlporlem  7196  nninfwlpoimlemg  7198  nninfwlpoim  7201  exmidonfinlem  7217  exmidfodomrlemr  7226  exmidfodomrlemrALT  7227  exmidaclem  7232  dju1en  7237  exmidontriimlem1  7245  exmidontriimlem3  7247  pw1on  7250  3nsssucpw1  7260  2omotaplemap  7281  2omotap  7283  exmidmotap  7285  cc4f  7293  cc4n  7295  dmaddpqlem  7401  nqpi  7402  dmaddpq  7403  dmmulpq  7404  ltdcnq  7421  subhalfnqq  7438  enq0sym  7456  enq0ref  7457  enq0tr  7458  nqnq0pi  7462  nq0nn  7466  addnq0mo  7471  mulnq0mo  7472  nqpnq0nq  7477  nqnq0a  7478  nqnq0m  7479  npsspw  7495  elnp1st2nd  7500  prnmaxl  7512  prnminu  7513  prarloc  7527  genprndl  7545  genprndu  7546  nqprm  7566  nqprl  7575  nqpru  7576  addnqprlemrl  7581  addnqprlemru  7582  prmuloc  7590  mulnqprlemrl  7597  mulnqprlemru  7598  ltsopr  7620  ltexprlemm  7624  ltexprlemopl  7625  ltexprlemopu  7627  lteupri  7641  recexprlemopl  7649  recexprlemopu  7651  recexprlemdisj  7654  archpr  7667  cauappcvgprlemdisj  7675  cauappcvgprlemladdrl  7681  cauappcvgprlem2  7684  caucvgprlemnbj  7691  caucvgprlemdisj  7698  caucvgprlemladdfu  7701  caucvgprlem2  7704  caucvgprprlemnbj  7717  caucvgprprlemdisj  7726  suplocexprlemml  7740  suplocexprlemrl  7741  suplocexprlemmu  7742  suplocexprlemloc  7745  addsrmo  7767  mulsrmo  7768  recexgt0sr  7797  prsrpos  7809  caucvgsrlemasr  7814  suplocsrlemb  7830  suplocsrlempr  7831  suplocsr  7833  elrealeu  7853  pitonn  7872  pitoregt0  7873  pitore  7874  recnnre  7875  axaddcl  7888  axaddrcl  7889  axmulcl  7890  axmulrcl  7891  axrnegex  7903  axcnre  7905  axpre-lttrn  7908  rereceu  7913  axarch  7915  axpre-suploclemres  7925  axpre-suploc  7926  ltxrlt  8048  apirr  8587  divmulasscomap  8678  rerecclap  8712  lbreu  8927  arch  9198  0mnnnnn0  9233  nnm1nn0  9242  elnnnn0c  9246  elnnz1  9301  ztri3or0  9320  nzadd  9330  nn0n0n1ge2  9348  zdceq  9353  zdcle  9354  zdclt  9355  uzind  9389  eluzge3nn  9597  supinfneg  9620  infsupneg  9621  eluz2b2  9628  elnn1uz2  9632  elnn0dc  9636  elnndc  9637  nn01to3  9642  znq  9649  qaddcl  9660  qmulcl  9662  qreccl  9667  irradd  9671  irrmul  9672  elpq  9673  cnref1o  9675  xnn0dcle  9827  xrpnfdc  9867  xrmnfdc  9868  xaddcom  9886  xnegdi  9893  xpncan  9896  xleadd1a  9898  iooidg  9934  elioo4g  9959  elfzd  10041  fzdcel  10065  fznlem  10066  fzpreddisj  10096  fz0to4untppr  10149  elfz0ubfz0  10150  elfz0fzfz0  10151  fz0fzelfz0  10152  fz0fzdiffz0  10155  elfzmlbp  10157  difelfzle  10159  4fvwrd4  10165  fzosplit  10202  elfzo0  10207  fzo1fzo0n0  10208  elfzonn0  10211  fzofzim  10213  elfzo1  10215  elfzom1elp1fzo  10227  fzossfzop1  10237  ssfzo12bi  10250  exfzdc  10265  qdceq  10272  exbtwnzlemstep  10273  exbtwnzlemex  10275  exbtwnz  10276  rebtwn2zlemstep  10278  rebtwn2z  10280  qbtwnxr  10283  modfzo0difsn  10421  frec2uzrand  10431  frec2uzf1od  10432  frecuzrdgrcl  10436  frecuzrdgtcl  10438  frecuzrdgrclt  10441  frecuzrdgfunlem  10445  frecfzennn  10452  seq3f1olemp  10528  seq3f1oleml  10529  ser0f  10541  expcl2lemap  10558  hashunsng  10814  shftfvalg  10854  shftfval  10857  caucvgre  11017  rexanuz  11024  recvguniq  11031  rennim  11038  resqrexlemf  11043  rsqrmo  11063  fimaxre2  11262  climeu  11331  sumdc  11393  summodc  11418  zsumdc  11419  isum  11420  fisumss  11427  isumss2  11428  fsumsplit  11442  sumsnf  11444  fsumsplitsn  11445  sumtp  11449  sumsplitdc  11467  fsum2dlemstep  11469  fisum0diag2  11482  fsumconst  11489  modfsummodlemstep  11492  fsum00  11497  fsumabs  11500  fsumiun  11512  isumlessdc  11531  expcnv  11539  prodmodc  11613  zproddc  11614  iprodap  11615  iprodap0  11617  fprodssdc  11625  prodsnf  11627  fprodsplitdc  11631  fprodsplit  11632  fprodm1  11633  fprod1p  11634  fprodunsn  11639  fprod2dlemstep  11657  fprodsplitsn  11668  ef0lem  11695  modmulconst  11857  dvdsdivcl  11883  dvdsssfz1  11885  dvdsfac  11893  zeoxor  11901  nn0ehalf  11935  nn0oddm1d2  11941  nnoddm1d2  11942  divalglemeunn  11953  divalglemeuneg  11955  zsupcllemstep  11973  infssuzex  11977  gcdsupex  11985  gcdsupcl  11986  bezoutlemnewy  12024  bezoutlemmain  12026  bezoutlemeu  12035  dfgcd2  12042  nnwosdc  12067  algrf  12072  algcvgblem  12076  lcmgcdlem  12104  lcmdvds  12106  coprmgcdb  12115  mulgcddvds  12121  qredeu  12124  cncongr1  12130  cncongr2  12131  isprm2lem  12143  dvdsnprmd  12152  prmdc  12157  oddprmge3  12162  pw2dvdseu  12195  phibndlem  12243  dfphi2  12247  hashdvds  12248  phiprmpw  12249  eulerthlemh  12258  hashgcdeq  12266  phisum  12267  odzdvds  12272  reumodprminv  12280  nnnn0modprm0  12282  prm23ge5  12291  pclemdc  12315  pcdvdsb  12347  difsqpwdvds  12365  oddprmdvds  12381  1arith  12394  4sqlem3  12417  4sqlemafi  12422  4sqlemffi  12423  4sqleminfi  12424  4sqexercise1  12425  4sqlem11  12428  4sqlem19  12436  ennnfonelemdc  12445  ennnfonelemh  12450  ennnfonelemhf1o  12459  ennnfonelemf1  12464  ennnfonelemrn  12465  ennnfonelemdm  12466  exmidunben  12472  ctinfomlemom  12473  ctinfom  12474  ctiunctlemudc  12483  ctiunctlemf  12484  ctiunctal  12487  nninfdclemcl  12494  nninfdclemf  12495  nninfdclemp1  12496  isstructim  12521  setsresg  12545  strleund  12608  1strbas  12622  2strbasg  12624  2stropg  12625  restsspw  12747  tgval  12760  ptex  12762  imasaddfnlemg  12784  fnpr2o  12808  fnpr2ob  12809  mgmidsssn0  12853  isnsgrp  12862  sgrpidmndm  12874  mndinvmod  12899  mnd1  12900  mhmeql  12937  grpinveu  12975  mulgval  13057  subgintm  13130  trivsubgsnd  13133  eqgfval  13154  ecqusaddd  13170  ecqusaddcl  13171  ghmeql  13199  iscmnd  13230  imasabl  13266  rnglz  13292  srgfcl  13320  reldvdsrsrg  13435  rhmopp  13519  subrgdvds  13575  lssuni  13672  lssintclm  13693  lspf  13698  qusmulrng  13839  mulgrhm2  13901  istopon  13950  toponcom  13964  topgele  13966  topontopn  13974  tsettps  13975  eltg2b  13991  unitg  13999  tgss2  14016  bastop2  14021  distop  14022  epttop  14027  cldss2  14043  neisspw  14085  neipsm  14091  neiuni  14098  tgcn  14145  tgcnp  14146  cnntr  14162  lmff  14186  txuni2  14193  txbasex  14194  txbas  14195  txcnp  14208  txcnmpt  14210  txcn  14212  txdis  14214  txdis1cn  14215  cnmpt11  14220  cnmpt12  14224  cnmpt21  14228  cnmpt2t  14230  cnmpt22  14231  blsscls2  14430  xmetxpbl  14445  xmettxlem  14446  tgqioo  14484  fsumcncntop  14493  cncfmpt1f  14521  mulcncflem  14527  mulcncf  14528  dedekindeu  14538  dedekindicclemicc  14547  dedekindicc  14548  ivthinclemdisj  14555  limcimo  14571  cnmptlimc  14580  reldvg  14585  dvfvalap  14587  dvfgg  14594  dveflem  14624  dvef  14625  sincn  14627  coscn  14628  reeff1o  14631  pilem3  14641  ioocosf1o  14712  lgsne0  14876  lgseisenlem2  14888  2sqlem2  14899  mul2sq  14900  2sqlem3  14901  2sqlem7  14905  bj-trst  14928  bj-fast  14930  bj-stand  14937  bj-trdc  14941  bj-fadc  14943  decidr  14985  djulclALT  14990  djurclALT  14991  bj-charfunr  14999  bj-indind  15121  bj-2inf  15127  bj-nntrans2  15141  bj-peano4  15144  bj-nnord  15147  bj-inf2vn  15163  bj-inf2vn2  15164  bj-findis  15168  pwf1oexmid  15187  subctctexmid  15188  nnsf  15192  nninfsellemdc  15197  nninffeq  15207  exmidsbthrlem  15208  sbthom  15212  triap  15215  trilpo  15229  apdifflemr  15233  redcwlpo  15241  tridceq  15242  nconstwlpolem0  15249  nconstwlpolem  15251  nconstwlpo  15252  neapmkv  15254  ltlenmkv  15256
  Copyright terms: Public domain W3C validator