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

Theorem sylbi 114
Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
sylbi.1
sylbi.2
Assertion
Ref Expression
sylbi

Proof of Theorem sylbi
StepHypRef Expression
1 sylbi.1 . . 3
21biimpi 113 . 2
3 sylbi.2 . 2
42, 3syl 14 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3imtr4i  190  mpan10  443  an12s  499  an32s  502  an4s  522  sylnbi  602  condc  748  notnot2dc  750  pm2.61ddc  757  pm5.18dc  776  dcim  783  pm2.25dc  791  pm2.85dc  810  pm5.12dc  815  pm5.14dc  816  pm5.55dc  818  peircedc  819  pm5.54dc  826  dcor  842  pm5.62dc  851  pm5.63dc  852  pm4.83dc  857  3simpb  901  3simpc  902  3imp  1097  3com12  1107  3com13  1108  syl3anb  1177  xoranor  1267  xorbin  1272  xordc1  1281  biassdc  1283  nfr  1408  nfand  1457  19.21t  1471  19.30dc  1515  exintrbi  1521  19.9t  1530  nfnt  1543  equveli  1639  exdistrfor  1678  sbcof2  1688  sbidm  1728  sbi1v  1768  sbalyz  1872  sbal1yz  1874  nfsb4t  1887  euex  1927  eumo0  1928  mor  1939  exmodc  1947  mo3h  1950  mopick  1975  moexexdc  1981  euexex  1982  2euex  1984  exists2  1994  eqcoms  2040  eleq2s  2129  nfcr  2167  necon3ai  2248  rexnalim  2311  rexex  2362  rsp  2363  ralim  2374  rexim  2407  r19.32r  2451  r19.44av  2463  r19.45av  2464  gencl  2580  gencbvex  2594  gencbval  2596  vtoclgf  2606  pm13.183  2675  elrabi  2689  eueq2dc  2708  eueq3dc  2709  mob2  2715  euxfr2dc  2720  reu3  2725  rmoim  2734  2rmorex  2739  sbcex  2766  ra5  2840  sseq1  2960  difdif  3063  difindiss  3185  undif3ss  3192  dfrab3ss  3209  abvor0dc  3236  reldisj  3265  disjel  3268  disj4im  3270  inssdif0im  3285  uneqdifeqim  3302  r19.2m  3303  r19.3rm  3304  r19.9rmv  3307  rexm  3314  ralm  3319  raaanlem  3320  ifnefalse  3336  nelpri  3388  prprc1  3469  difprsn2  3495  diftpsn3  3496  snsssn  3523  preqr2  3531  preq12b  3532  opthpr  3534  prneimg  3536  oprcl  3564  pwprss  3567  intmin4  3634  uniintabim  3643  dfiin2g  3681  iinss2  3700  iundif2ss  3713  invdisj  3750  trel  3852  trss  3854  ssex  3885  bnd2  3917  abssexg  3925  rext  3942  unipw  3944  euabex  3952  mss  3953  exss  3954  copsexg  3972  opelopabsb  3988  pwssunim  4012  epelg  4018  sowlin  4048  sotritric  4052  elsuci  4106  sucprc  4115  reusv3  4158  ordon  4178  onsucmin  4198  onsucelsucr  4199  unon  4202  onsucelsucexmid  4215  setind  4222  setind2  4223  sucprcreg  4227  en2lp  4232  eunex  4239  ordsoexmid  4240  ordpwsucss  4243  tfi  4248  peano1  4260  peano2  4261  find  4265  0nelelxp  4316  opelxp  4317  elvvuni  4347  optocl  4359  ralxpf  4425  rexxpf  4426  relop  4429  breldm  4482  dmxpm  4498  elreldm  4503  dmrnssfld  4538  dmcosseq  4546  resabs1  4583  resima2  4587  issref  4650  asymref  4653  xpidtr  4658  trin2  4659  poirr2  4660  xpmlem  4687  dmxpss  4696  xp11m  4702  cnveqb  4719  dfco2a  4764  cores2  4776  coi2  4780  relcnvtr  4783  relresfld  4790  relcnvexb  4800  cnviinm  4802  iotauni  4822  iota1  4824  iota4  4828  dffun8  4872  funcnvsn  4888  imadif  4922  imainlem  4923  fcoi1  5013  fcoi2  5014  f1ocnv  5082  f1ocnvb  5083  fun11iun  5090  ffoss  5101  f1o00  5104  fo00  5105  relelfvdm  5148  nfvres  5149  nfunsn  5150  ssimaex  5177  fvmptss2  5190  fvmptssdm  5198  unpreima  5235  respreima  5238  elrnrexdm  5249  elrnrexdmb  5250  rexrnmpt  5253  dffo4  5258  rnmptss  5269  fvpr1  5308  fvpr2  5309  elunirn  5348  f1veqaeq  5351  isores1  5397  riotauni  5417  riotacl2  5424  riota1  5429  riota1a  5430  snriota  5440  eusvobj2  5441  acexmidlema  5446  acexmidlemb  5447  acexmidlem2  5452  oprabid  5480  0neqopab  5492  brabvv  5493  1stval2  5724  2ndval2  5725  xp1st  5734  xp2nd  5735  unielxp  5742  releldm2  5753  cnvf1o  5788  fo2ndf  5790  poxp  5794  reldmtpos  5809  dftpos4  5819  tpostpos  5820  tpostpos2  5821  iunon  5840  smoel  5856  tfrlem4  5870  tfrlem7  5874  tfrlem8  5875  tfrlem9  5876  nnaord  6018  ecexr  6047  swoord1  6071  swoord2  6072  0er  6076  idssen  6193  ener  6195  en0  6211  en1  6215  en1bg  6216  2dom  6221  enm  6230  xpsnen  6231  indpi  6326  subhalfnqq  6397  archnqq  6400  enq0sym  6415  nqnq0pi  6421  nqnq0  6424  mulnnnq0  6433  prml  6460  prmu  6461  prssnql  6462  prssnqu  6463  prcdnql  6467  prcunqu  6468  prltlu  6470  prnmaxl  6471  prnminu  6472  prloc  6474  prdisj  6475  addcanprg  6590  recexprlemopl  6597  recexprlemopu  6599  cauappcvgprlemladdfu  6626  caucvgprlemladdfu  6648  recexgt0sr  6701  renfdisj  6876  recexre  7362  apsqgt0  7385  apreim  7387  recexaplem2  7415  rerecclap  7488  nn0ge0  7983  elnnnn0b  8002  znegcl  8052  zeo  8119  nn0ind  8128  nn0ind-raph  8131  uzn0  8264  eluzaddi  8275  eluzsubi  8276  uznn0sub  8280  uz3m2nn  8291  uznnssnn  8296  uz2m1nn  8318  uz2mulcl  8321  indstr2  8322  qmulz  8334  qre  8336  qnegcl  8347  qreccl  8351  rphalflt  8387  xrltnr  8471  nltpnft  8500  ngtmnft  8501  xrrebnd  8502  xnegcl  8515  xnegneg  8516  xltnegi  8518  elioore  8551  elfzuz2  8663  uzsubsubfz  8681  fzdisj  8686  fzmmmeqm  8691  elfz0ubfz0  8752  elfz0fzfz0  8753  fz0fzelfz0  8754  fz0fzdiffz0  8757  elfzmlbp  8760  difelfzle  8762  difelfznle  8763  nn0disj  8765  2ffzeq  8768  fzo1fzo0n0  8809  elfzo0z  8810  elfzo0le  8811  fzonmapblen  8813  fzofzim  8814  elfzodifsumelfzo  8827  elfzonlteqm1  8836  fzonn0p1p1  8839  elfzom1p1elfzo  8840  ssfzo12bi  8851  ubmelm1fzo  8852  fzind2  8865  expcl2lemap  8921  qexpclz  8930  bj-nfalt  9239  bdel  9300  bdssex  9353  findset  9399
  Copyright terms: Public domain W3C validator