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

Theorem sylibr 132
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 (𝜑𝜓)
sylibr.2 (𝜒𝜓)
Assertion
Ref Expression
sylibr (𝜑𝜒)

Proof of Theorem sylibr
StepHypRef Expression
1 sylibr.1 . 2 (𝜑𝜓)
2 sylibr.2 . . 3 (𝜒𝜓)
32biimpri 131 . 2 (𝜓𝜒)
41, 3syl 14 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  sylbbr  134  pm5.74rd  181  bitri  182  3imtr4i  199  sylanbrc  408  dcimpstab  786  dcim  818  oibabs  834  stabtestimpdc  858  dcor  877  3mix1  1108  3mix2  1109  3jca  1119  syl3anbrc  1123  inegd  1304  pclem6  1306  xoranor  1309  nfxfrd  1405  nfd  1457  hban  1480  nfan1  1497  nford  1500  nfand  1501  hbim1  1503  alexim  1577  ax6blem  1581  nf4r  1602  19.34  1615  nfexd  1685  sbcof2  1732  nfsb2or  1759  sbidm  1773  nfdv  1799  nfeudv  1957  mon  1971  eumo  1974  mo23  1983  eu2  1986  eu3h  1987  exmodc  1992  exmonim  1993  mo2r  1994  mo3h  1995  bm1.1  2067  eqrdv  2080  3eltr4g  2165  abbi2dv  2198  abbi1dv  2199  nfcd  2215  nfcxfrd  2218  dcned  2252  neqned  2253  3netr4g  2281  necon3bi  2296  necon2ai  2300  alral  2410  rspe  2413  rsp2e  2415  rgen2a  2418  ralrimi  2433  r19.27av  2493  r19.32r  2502  nfreudxy  2528  mormo  2566  nrexrmo  2571  cgsex2g  2636  cgsex4g  2637  spc2egv  2688  spc2gv  2689  spc3egv  2690  spc3gv  2691  rspce  2697  ceqex  2723  elrab3t  2749  mosubt  2770  mo2icl  2772  reu3  2783  reu6i  2784  2rmorex  2797  sbc5  2839  rspesbca  2899  rmo2ilem  2904  sbnfc2  2963  ssrd  3005  ssrdv  3006  3sstr4g  3041  syl5eqss  3044  ss2abdv  3068  abssdv  3069  rabssdv  3075  ss2rabdv  3076  ssun1  3136  unssad  3150  unssbd  3151  ssddif  3205  uneqin  3222  indifdir  3227  undif3ss  3232  reuss2  3251  n0rf  3267  reximdva0m  3270  rabxmdc  3283  ssindif0im  3310  minel  3312  ralidm  3349  ralm  3353  disjsn2  3463  absneu  3472  rabsneu  3473  opprc  3599  elunii  3614  dfnfc2  3627  uniss2  3640  unidif  3641  ssunieq  3642  intab  3673  iunss2  3731  iunxdif2  3734  invdisj  3788  3brtr4g  3825  trin  3893  triun  3896  truni  3897  trint  3898  iinexgm  3937  class2seteq  3945  pwuni  3971  mss  3989  copsex2t  4008  euotd  4017  pwunim  4049  ispod  4067  sotricim  4086  exse  4099  frind  4115  trssord  4143  suctr  4184  eusvnf  4211  eusvnfb  4212  eusv2nf  4214  rexxfrd  4221  ralxfr2d  4222  rexxfr2d  4223  rabxfrd  4227  reuhypd  4229  eldifpw  4234  iunpw  4237  ssorduni  4239  sucelon  4255  onsucelsucr  4260  sucunielr  4262  ordtri2or2exmidlem  4277  onsucelsucexmid  4281  reg2exmidlema  4285  setindel  4289  elirr  4292  orddisj  4297  en2lp  4305  suc11g  4308  ordsuc  4314  nlimsucg  4317  ordtri2or2exmid  4322  zfregfr  4324  wessep  4328  tfi  4331  peano5  4347  limom  4362  peano2b  4363  nndceq0  4365  eqrelrdv  4462  xpsspw  4478  relint  4489  relop  4514  eqbrrdva  4533  opeldm  4566  elres  4674  relssres  4676  exse2  4729  issref  4737  trin2  4746  dminss  4768  imainss  4769  rnxpid  4785  dmsn0el  4820  dmmptg  4848  relrelss  4874  cnviinm  4889  iotanul  4912  sniota  4924  dffun5r  4944  funmo  4947  funco  4970  funun  4974  funprg  4980  funtpg  4981  funtp  4983  fntpg  4986  fununi  4998  funcnvuni  4999  imadiflem  5009  imainlem  5011  funimaexglem  5013  isarep2  5017  fnunsn  5037  2elresin  5041  fnimadisj  5050  fco  5087  funssxp  5091  fssres  5097  feu  5103  fimacnvdisj  5105  fabexg  5108  f00  5112  f1co  5132  fores  5146  foco  5147  f1ores  5172  foimacnv  5175  f1oun  5177  fun11iun  5178  f1oco  5180  fo00  5193  brprcneu  5202  fv3  5229  relelfvdm  5237  nfvres  5238  nfunsn  5239  funfvbrb  5312  respreima  5327  dff2  5343  dff3im  5344  dffo4  5347  ffvresb  5360  f1oresrab  5361  fmptco  5362  fsn  5367  fpr  5377  ftpg  5379  fsnunf  5394  fsnunfv  5395  elabrex  5429  dff1o6  5447  foeqcnvco  5461  fliftel1  5465  isores1  5485  isoini2  5489  riotasbc  5514  acexmidlemph  5536  acexmidlemcase  5538  oprabidlem  5567  brabvv  5582  eloprabga  5622  fnoprabg  5633  caovimo  5725  oprabexd  5785  fo1stresm  5819  fo2ndresm  5820  unielxp  5831  1st2ndbr  5841  fmpt2co  5868  1stconst  5873  2ndconst  5874  poxp  5884  spc2ed  5885  reldmtpos  5902  tposfun  5909  dftpos4  5912  smores  5941  smores2  5943  tfrlem1  5957  tfr0dm  5971  tfrlemibxssdm  5976  tfrlemibex  5978  tfrlemiubacc  5979  tfrlemi14d  5982  tfrexlem  5983  tfri1d  5984  tfr1onlembxssdm  5992  tfr1onlembex  5994  tfr1onlemubacc  5995  tfr1onlemres  5998  tfrcllemsucfn  6002  tfrcllembxssdm  6005  tfrcllembex  6007  tfrcllemubacc  6008  tfrcllemres  6011  tfri3  6016  rdgon  6035  frecabcl  6048  frecfcllem  6053  frecrdg  6057  2oconcl  6086  nnsucelsuc  6135  nntri3or  6137  nndceq  6143  nndcel  6144  nndifsnid  6146  ecexr  6177  brdifun  6199  ecelqsdm  6242  iinerm  6244  eroveu  6263  erovlem  6264  ecopovtrn  6269  ecopovtrng  6272  th3qlem1  6274  f1oen3g  6301  ssdomg  6325  domtr  6332  snfig  6359  xpf1o  6385  php5dom  6398  fidceq  6404  fidifsnid  6406  nnfi  6407  fiunsnnn  6415  findcard  6422  findcard2  6423  findcard2s  6424  ac6sfi  6431  nnwetri  6436  unsnfi  6439  unsnfidcex  6440  unsnfidcel  6441  supmoti  6465  dmaddpqlem  6629  nqpi  6630  dmaddpq  6631  dmmulpq  6632  ltdcnq  6649  subhalfnqq  6666  enq0sym  6684  enq0ref  6685  enq0tr  6686  nqnq0pi  6690  nq0nn  6694  addnq0mo  6699  mulnq0mo  6700  nqpnq0nq  6705  nqnq0a  6706  nqnq0m  6707  npsspw  6723  elnp1st2nd  6728  prnmaxl  6740  prnminu  6741  prarloc  6755  genprndl  6773  genprndu  6774  nqprm  6794  nqprl  6803  nqpru  6804  addnqprlemrl  6809  addnqprlemru  6810  prmuloc  6818  mulnqprlemrl  6825  mulnqprlemru  6826  ltsopr  6848  ltexprlemm  6852  ltexprlemopl  6853  ltexprlemopu  6855  lteupri  6869  recexprlemopl  6877  recexprlemopu  6879  recexprlemdisj  6882  archpr  6895  cauappcvgprlemdisj  6903  cauappcvgprlemladdrl  6909  cauappcvgprlem2  6912  caucvgprlemnbj  6919  caucvgprlemdisj  6926  caucvgprlemladdfu  6929  caucvgprlem2  6932  caucvgprprlemnbj  6945  caucvgprprlemdisj  6954  addsrmo  6982  mulsrmo  6983  recexgt0sr  7012  prsrpos  7023  caucvgsrlemasr  7028  elrealeu  7060  pitonn  7078  pitoregt0  7079  pitore  7080  recnnre  7081  axaddcl  7094  axaddrcl  7095  axmulcl  7096  axmulrcl  7097  axrnegex  7107  axcnre  7109  axpre-lttrn  7112  rereceu  7117  axarch  7119  ltxrlt  7245  apirr  7772  divmulasscomap  7851  rerecclap  7885  lbreu  8090  arch  8352  0mnnnnn0  8387  nnm1nn0  8396  elnnnn0c  8400  elnnz1  8455  ztri3or0  8474  nzadd  8484  nn0n0n1ge2  8499  zdceq  8504  zdcle  8505  zdclt  8506  uzind  8539  eluzge3nn  8741  supinfneg  8764  infsupneg  8765  eluz2b2  8771  elnn1uz2  8775  nn01to3  8783  znq  8790  qaddcl  8801  qmulcl  8803  qreccl  8808  irradd  8812  irrmul  8813  cnref1o  8814  iooidg  9008  elioo4g  9033  fzdcel  9135  fznlem  9136  fzpreddisj  9164  elfz0ubfz0  9213  elfz0fzfz0  9214  fz0fzelfz0  9215  fz0fzdiffz0  9218  elfzmlbp  9220  difelfzle  9222  4fvwrd4  9227  fzosplit  9263  elfzo0  9268  fzo1fzo0n0  9269  elfzonn0  9272  fzofzim  9274  elfzo1  9276  elfzom1elp1fzo  9288  fzossfzop1  9298  ssfzo12bi  9311  exfzdc  9326  qdceq  9333  exbtwnzlemstep  9334  exbtwnzlemex  9336  exbtwnz  9337  rebtwn2zlemstep  9339  rebtwn2z  9341  qbtwnxr  9344  modfzo0difsn  9477  frec2uzrand  9487  frec2uzf1od  9488  frecuzrdgrcl  9492  frecuzrdgtcl  9494  frecuzrdgrclt  9497  frecuzrdgfunlem  9501  frecfzennn  9508  iseqfcl  9535  iser0f  9569  expcl2lemap  9585  sizeunsng  9831  shftfvalg  9844  shftfval  9847  caucvgre  10005  rexanuz  10012  recvguniq  10019  rennim  10026  resqrexlemf  10031  rsqrmo  10051  fimaxre2  10247  climeu  10273  sumdc  10333  modmulconst  10372  dvdsdivcl  10395  dvdsssfz1  10397  dvdsfac  10405  zeoxor  10413  nn0ehalf  10447  nn0oddm1d2  10453  nnoddm1d2  10454  divalglemeunn  10465  divalglemeuneg  10467  zsupcllemstep  10485  infssuzex  10489  gcdsupex  10493  gcdsupcl  10494  bezoutlemnewy  10529  bezoutlemmain  10531  bezoutlemeu  10540  dfgcd2  10547  ialgrf  10571  algcvgblem  10575  lcmgcdlem  10603  lcmdvds  10605  coprmgcdb  10614  mulgcddvds  10620  qredeu  10623  cncongr1  10629  cncongr2  10630  isprm2lem  10642  dvdsnprmd  10651  oddprmge3  10660  pw2dvdseu  10690  bj-nfalt  10726  decidr  10757  bj-indind  10885  bj-2inf  10891  bj-nntrans2  10905  bj-peano4  10908  bj-nnord  10911  bj-inf2vn  10927  bj-inf2vn2  10928  bj-findis  10932
  Copyright terms: Public domain W3C validator