ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylbi GIF 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  603  condc  749  notnotrdc  751  pm2.61ddc  758  pm5.18dc  777  dcim  784  pm2.25dc  792  pm2.85dc  811  pm5.12dc  816  pm5.14dc  817  pm5.55dc  819  peircedc  820  pm5.54dc  827  dcor  843  pm5.62dc  852  pm5.63dc  853  pm4.83dc  858  3simpb  902  3simpc  903  3imp  1098  3com12  1108  3com13  1109  syl3anb  1178  xoranor  1268  xorbin  1275  xordc1  1284  biassdc  1286  nfr  1411  nfand  1460  19.21t  1474  19.30dc  1518  exintrbi  1524  19.9t  1533  nfnt  1546  equveli  1642  exdistrfor  1681  sbcof2  1691  sbidm  1731  sbi1v  1771  sbalyz  1875  sbal1yz  1877  nfsb4t  1890  euex  1930  eumo0  1931  mor  1942  exmodc  1950  mo3h  1953  mopick  1978  moexexdc  1984  euexex  1985  2euex  1987  exists2  1997  eqcoms  2043  eleq2s  2132  nfcr  2170  necon3ai  2254  rexnalim  2317  rexex  2368  rsp  2369  ralim  2380  rexim  2413  r19.32r  2457  r19.44av  2469  r19.45av  2470  gencl  2586  gencbvex  2600  gencbval  2602  vtoclgf  2612  pm13.183  2681  elrabi  2695  eueq2dc  2714  eueq3dc  2715  mob2  2721  euxfr2dc  2726  reu3  2731  rmoim  2740  2rmorex  2745  sbcex  2772  ra5  2846  sseq1  2966  difdif  3069  difindiss  3191  undif3ss  3198  dfrab3ss  3215  abvor0dc  3242  reldisj  3271  disjel  3274  disj4im  3276  inssdif0im  3291  uneqdifeqim  3308  r19.2m  3309  r19.3rm  3310  r19.9rmv  3313  rexm  3320  ralm  3325  raaanlem  3326  ifnefalse  3342  nelpri  3399  prprc1  3478  difprsn2  3504  diftpsn3  3505  snsssn  3532  preqr2  3540  preq12b  3541  opthpr  3543  prneimg  3545  oprcl  3573  pwprss  3576  intmin4  3643  uniintabim  3652  dfiin2g  3690  iinss2  3709  iundif2ss  3722  invdisj  3759  trel  3861  trss  3863  ssex  3894  bnd2  3926  abssexg  3934  rext  3951  unipw  3953  euabex  3961  mss  3962  exss  3963  copsexg  3981  opelopabsb  3997  pwssunim  4021  epelg  4027  sowlin  4057  sotritric  4061  elsuci  4140  sucprc  4149  reusv3  4192  ordon  4212  onsucmin  4233  onsucelsucr  4234  unon  4237  onsucelsucexmid  4255  setind  4264  setind2  4265  sucprcreg  4273  en2lp  4278  eunex  4285  ordsoexmid  4286  ordpwsucss  4291  tfi  4305  peano1  4317  peano2  4318  find  4322  0nelelxp  4373  opelxp  4374  elvvuni  4404  optocl  4416  ralxpf  4482  rexxpf  4483  relop  4486  breldm  4539  dmxpm  4555  elreldm  4560  dmrnssfld  4595  dmcosseq  4603  resabs1  4640  resima2  4644  issref  4707  asymref  4710  xpidtr  4715  trin2  4716  poirr2  4717  xpmlem  4744  dmxpss  4753  xp11m  4759  cnveqb  4776  dfco2a  4821  cores2  4833  coi2  4837  relcnvtr  4840  relresfld  4847  relcnvexb  4857  cnviinm  4859  iotauni  4879  iota1  4881  iota4  4885  dffun8  4929  funcnvsn  4945  imadif  4979  imainlem  4980  fcoi1  5070  fcoi2  5071  f1ocnv  5139  f1ocnvb  5140  fun11iun  5147  ffoss  5158  f1o00  5161  fo00  5162  relelfvdm  5205  nfvres  5206  nfunsn  5207  ssimaex  5234  fvmptss2  5247  fvmptssdm  5255  unpreima  5292  respreima  5295  elrnrexdm  5306  elrnrexdmb  5307  rexrnmpt  5310  dffo4  5315  rnmptss  5326  fvpr1  5365  fvpr2  5366  elunirn  5405  f1veqaeq  5408  isores1  5454  riotauni  5474  riotacl2  5481  riota1  5486  riota1a  5487  snriota  5497  eusvobj2  5498  acexmidlema  5503  acexmidlemb  5504  acexmidlem2  5509  oprabid  5537  0neqopab  5550  brabvv  5551  1stval2  5782  2ndval2  5783  xp1st  5792  xp2nd  5793  unielxp  5800  releldm2  5811  cnvf1o  5846  fo2ndf  5848  poxp  5853  reldmtpos  5868  dftpos4  5878  tpostpos  5879  tpostpos2  5880  iunon  5899  smoel  5915  tfrlem4  5929  tfrlem7  5933  tfrlem8  5934  tfrlem9  5935  nnaord  6082  ecexr  6111  swoord1  6135  swoord2  6136  0er  6140  idssen  6257  ener  6259  en0  6275  en1  6279  en1bg  6280  2dom  6285  enm  6294  xpsnen  6295  snnen2og  6322  php5dom  6325  phpm  6327  findcard  6345  findcard2  6346  findcard2s  6347  finnum  6361  indpi  6438  subhalfnqq  6510  archnqq  6513  enq0sym  6528  nqnq0pi  6534  nqnq0  6537  mulnnnq0  6546  prml  6573  prmu  6574  prssnql  6575  prssnqu  6576  prcdnql  6580  prcunqu  6581  prltlu  6583  prnmaxl  6584  prnminu  6585  prloc  6587  prdisj  6588  addcanprg  6712  recexprlemopl  6721  recexprlemopu  6723  cauappcvgprlemladdfu  6750  caucvgprlemladdfu  6773  recexgt0sr  6856  renfdisj  7077  recexre  7567  apsqgt0  7590  apreim  7592  recexaplem2  7631  rerecclap  7704  nn0ge0  8205  elnnnn0b  8224  znegcl  8274  zeo  8341  nn0ind  8350  nn0ind-raph  8353  uzn0  8486  eluzaddi  8497  eluzsubi  8498  uznn0sub  8502  uz3m2nn  8513  uznnssnn  8518  uz2m1nn  8540  uz2mulcl  8543  indstr2  8544  qmulz  8556  qre  8558  qnegcl  8569  qreccl  8574  rphalflt  8610  xrltnr  8699  nltpnft  8728  ngtmnft  8729  xrrebnd  8730  xnegcl  8743  xnegneg  8744  xltnegi  8746  elioore  8779  elfzuz2  8891  uzsubsubfz  8909  fzdisj  8914  fzmmmeqm  8919  elfz0ubfz0  8980  elfz0fzfz0  8981  fz0fzelfz0  8982  fz0fzdiffz0  8985  elfzmlbp  8988  difelfzle  8990  difelfznle  8991  nn0disj  8993  2ffzeq  8996  fzo1fzo0n0  9037  elfzo0z  9038  elfzo0le  9039  fzonmapblen  9041  fzofzim  9042  elfzodifsumelfzo  9055  elfzonlteqm1  9064  fzonn0p1p1  9067  elfzom1p1elfzo  9068  ssfzo12bi  9079  ubmelm1fzo  9080  fzind2  9093  subfzo0  9095  rebtwn2z  9107  fldiv4p1lem1div2  9145  flqeqceilz  9158  expcl2lemap  9241  qexpclz  9250  cvg1nlemres  9558  rexanuz  9561  fclim  9789  climmo  9793  ialgfx  9865  bj-nfalt  9878  bdel  9939  bdssex  9996  bj-indind  10030  findset  10044
  Copyright terms: Public domain W3C validator