ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylbi 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  |-  ( ph  <->  ps )
sylbi.2  |-  ( ps 
->  ch )
Assertion
Ref Expression
sylbi  |-  ( ph  ->  ch )

Proof of Theorem sylbi
StepHypRef Expression
1 sylbi.1 . . 3  |-  ( ph  <->  ps )
21biimpi 113 . 2  |-  ( ph  ->  ps )
3 sylbi.2 . 2  |-  ( ps 
->  ch )
42, 3syl 14 1  |-  ( ph  ->  ch )
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  6363  indpi  6440  subhalfnqq  6512  archnqq  6515  enq0sym  6530  nqnq0pi  6536  nqnq0  6539  mulnnnq0  6548  prml  6575  prmu  6576  prssnql  6577  prssnqu  6578  prcdnql  6582  prcunqu  6583  prltlu  6585  prnmaxl  6586  prnminu  6587  prloc  6589  prdisj  6590  addcanprg  6714  recexprlemopl  6723  recexprlemopu  6725  cauappcvgprlemladdfu  6752  caucvgprlemladdfu  6775  recexgt0sr  6858  renfdisj  7079  recexre  7569  apsqgt0  7592  apreim  7594  recexaplem2  7633  rerecclap  7706  nn0ge0  8207  elnnnn0b  8226  znegcl  8276  zeo  8343  nn0ind  8352  nn0ind-raph  8355  uzn0  8488  eluzaddi  8499  eluzsubi  8500  uznn0sub  8504  uz3m2nn  8515  uznnssnn  8520  uz2m1nn  8542  uz2mulcl  8545  indstr2  8546  qmulz  8558  qre  8560  qnegcl  8571  qreccl  8576  rphalflt  8612  xrltnr  8701  nltpnft  8730  ngtmnft  8731  xrrebnd  8732  xnegcl  8745  xnegneg  8746  xltnegi  8748  elioore  8781  elfzuz2  8893  uzsubsubfz  8911  fzdisj  8916  fzmmmeqm  8921  elfz0ubfz0  8982  elfz0fzfz0  8983  fz0fzelfz0  8984  fz0fzdiffz0  8987  elfzmlbp  8990  difelfzle  8992  difelfznle  8993  nn0disj  8995  2ffzeq  8998  fzo1fzo0n0  9039  elfzo0z  9040  elfzo0le  9041  fzonmapblen  9043  fzofzim  9044  elfzodifsumelfzo  9057  elfzonlteqm1  9066  fzonn0p1p1  9069  elfzom1p1elfzo  9070  ssfzo12bi  9081  ubmelm1fzo  9082  fzind2  9095  subfzo0  9097  rebtwn2z  9109  fldiv4p1lem1div2  9147  flqeqceilz  9160  expcl2lemap  9267  qexpclz  9276  cvg1nlemres  9584  rexanuz  9587  fclim  9815  climmo  9819  ialgfx  9891  bj-nfalt  9904  bdel  9965  bdssex  10022  bj-indind  10056  findset  10070
  Copyright terms: Public domain W3C validator