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

Theorem sylbi 119
Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 3-Jan-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 118 . 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 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  sylbb  121  sylbb2  136  3imtr4i  199  simplbiim  379  mpan10  458  an12s  530  an32s  533  an4s  553  sylnbi  636  condc  783  notnotrdc  785  pm2.61ddc  792  pm5.18dc  811  dcim  818  pm2.25dc  826  pm2.85dc  845  pm5.12dc  850  pm5.14dc  851  pm5.55dc  853  peircedc  854  pm5.54dc  861  dcor  877  pm5.62dc  887  pm5.63dc  888  pm4.83dc  893  3simpb  937  3simpc  938  3imp  1133  3com12  1143  3com13  1144  syl3anb  1213  xoranor  1309  xorbin  1316  xordc1  1325  biassdc  1327  nfr  1452  nfand  1501  19.21t  1515  19.30dc  1559  exintrbi  1565  19.9t  1574  nfnt  1587  equveli  1684  exdistrfor  1723  sbcof2  1733  sbidm  1774  sbi1v  1814  sbalyz  1918  sbal1yz  1920  nfsb4t  1933  euex  1973  eumo0  1974  mor  1985  exmodc  1993  mo3h  1996  mopick  2021  moexexdc  2027  euexex  2028  2euex  2030  exists2  2040  eqcoms  2086  eleq2s  2177  nfcr  2215  necon3ai  2298  rexnalim  2364  rexex  2415  rsp  2416  ralim  2427  rexim  2460  r19.32r  2506  r19.44av  2518  r19.45av  2519  gencl  2640  gencbvex  2654  gencbval  2656  vtoclgf  2666  pm13.183  2740  elrabi  2754  eueq2dc  2774  eueq3dc  2775  mob2  2781  euxfr2dc  2786  reu3  2791  rmoim  2800  2rmorex  2805  sbcex  2832  sbcbi2  2873  ra5  2911  sseq1  3029  difdif  3107  difindiss  3234  undif3ss  3241  dfrab3ss  3258  abvor0dc  3285  reldisj  3311  disjel  3314  inssdif0im  3327  uneqdifeqim  3344  r19.2m  3345  r19.3rm  3346  r19.9rmv  3349  rexm  3357  ralm  3362  raaanlem  3363  ifnefalse  3379  nelpri  3440  prprc1  3518  difprsn2  3545  diftpsn3  3546  snsssn  3573  preqr2  3581  preq12b  3582  opthpr  3584  prneimg  3586  oprcl  3614  pwprss  3617  intmin4  3684  uniintabim  3693  dfiin2g  3731  iinss2  3750  iundif2ss  3763  invdisj  3800  trel  3902  trss  3904  ssex  3935  bnd2  3967  abssexg  3975  exmidexmid  3987  rext  3998  unipw  4000  euabex  4008  mss  4009  exss  4010  copsexg  4027  opelopabsb  4043  pwssunim  4067  epelg  4073  sowlin  4103  sotritric  4107  elsuci  4186  sucprc  4195  reusv3  4238  ordon  4258  onsucmin  4279  onsucelsucr  4280  unon  4283  onsucelsucexmid  4301  setind  4310  setind2  4311  sucprcreg  4320  en2lp  4325  eunex  4332  ordsoexmid  4333  ordpwsucss  4338  tfi  4351  peano1  4363  peano2  4364  find  4368  0nelelxp  4419  opelxp  4420  elvvuni  4450  optocl  4462  ralxpf  4530  rexxpf  4531  relop  4534  breldm  4587  dmxpm  4603  elreldm  4608  dmrnssfld  4643  dmcosseq  4651  resabs1  4688  resima2  4692  issref  4757  asymref  4760  xpidtr  4765  trin2  4766  poirr2  4767  xpmlem  4794  dmxpss  4803  xp11m  4809  cnveqb  4826  dfco2a  4871  cores2  4883  coi2  4887  relcnvtr  4890  relresfld  4897  relcnvexb  4907  cnviinm  4909  iotauni  4929  iota1  4931  iota4  4935  dffun8  4979  funcnvsn  4995  imadif  5030  imainlem  5031  fcoi1  5121  fcoi2  5122  f1ocnv  5190  f1ocnvb  5191  fun11iun  5198  ffoss  5209  f1o00  5212  fo00  5213  relelfvdm  5257  nfvres  5258  nfunsn  5259  ssimaex  5286  fvmptss2  5299  fvmptssdm  5307  unpreima  5344  respreima  5347  elrnrexdm  5358  elrnrexdmb  5359  rexrnmpt  5362  dffo4  5367  rnmptss  5378  fvpr1  5417  fvpr2  5418  elunirn  5457  f1veqaeq  5460  isores1  5505  riotauni  5525  riotacl2  5532  riota1  5537  riota1a  5538  snriota  5548  eusvobj2  5549  acexmidlema  5554  acexmidlemb  5555  acexmidlem2  5560  oprabid  5588  0neqopab  5601  brabvv  5602  1stval2  5833  2ndval2  5834  xp1st  5843  xp2nd  5844  unielxp  5851  releldm2  5862  cnvf1o  5897  fo2ndf  5899  poxp  5904  reldmtpos  5922  dftpos4  5932  tpostpos  5933  tpostpos2  5934  iunon  5953  smoel  5969  tfrlem4  5982  tfrlem7  5986  tfrlem8  5987  tfrlem9  5988  nnaord  6169  ecexr  6198  swoord1  6222  swoord2  6223  0er  6227  idssen  6345  ener  6347  en0  6363  en1  6367  en1bg  6368  2dom  6373  enm  6385  xpsnen  6386  snnen2og  6415  php5dom  6419  phpm  6421  findcard  6444  findcard2  6445  findcard2s  6446  unfiexmid  6462  djuun  6558  finnum  6563  indpi  6646  subhalfnqq  6718  archnqq  6721  enq0sym  6736  nqnq0pi  6742  nqnq0  6745  mulnnnq0  6754  prml  6781  prmu  6782  prssnql  6783  prssnqu  6784  prcdnql  6788  prcunqu  6789  prltlu  6791  prnmaxl  6792  prnminu  6793  prloc  6795  prdisj  6796  addcanprg  6920  recexprlemopl  6929  recexprlemopu  6931  cauappcvgprlemladdfu  6958  caucvgprlemladdfu  6981  recexgt0sr  7064  renfdisj  7291  negf1o  7605  recexre  7797  apsqgt0  7820  apreim  7822  recexaplem2  7861  rerecclap  7937  nn0ge0  8432  elnnnn0b  8451  xnn0xr  8475  xnn0nemnf  8481  xnn0nnn0pnf  8483  znegcl  8515  zeo  8585  nn0ind  8594  nn0ind-raph  8597  uzn0  8767  eluzaddi  8778  eluzsubi  8779  uznn0sub  8783  uz3m2nn  8794  uznnssnn  8798  uz2m1nn  8825  uz2mulcl  8828  indstr2  8829  qmulz  8841  qre  8843  qnegcl  8854  qreccl  8860  rphalflt  8896  nn0ledivnn  8971  xrltnr  8983  nltpnft  9012  ngtmnft  9013  xrrebnd  9014  xnegcl  9027  xnegneg  9028  xltnegi  9030  elioore  9063  elfzuz2  9176  uzsubsubfz  9194  fzdisj  9199  fzmmmeqm  9204  elfz0ubfz0  9265  elfz0fzfz0  9266  fz0fzelfz0  9267  fz0fzdiffz0  9270  elfzmlbp  9272  difelfzle  9274  difelfznle  9275  nn0disj  9277  2ffzeq  9280  fzo1fzo0n0  9321  elfzo0z  9322  elfzo0le  9323  fzonmapblen  9325  fzofzim  9326  elfzodifsumelfzo  9339  elfzonlteqm1  9348  fzonn0p1p1  9351  elfzom1p1elfzo  9352  ssfzo12bi  9363  ubmelm1fzo  9364  fzind2  9377  subfzo0  9380  rebtwn2z  9393  fldiv4p1lem1div2  9439  flqeqceilz  9452  zmodidfzoimp  9488  modfzo0difsn  9529  nnsinds  9571  nn0sinds  9572  expcl2lemap  9637  qexpclz  9646  facp1  9806  facnn2  9810  faclbnd3  9819  bcn1  9834  hashfz0  9901  cvg1nlemres  10072  rexanuz  10075  fclim  10334  climmo  10338  dvdsdivcl  10458  addmodlteqALT  10467  odd2np1  10480  oddge22np1  10488  m1expe  10506  nn0enne  10509  nn0o1gt2  10512  nno  10513  ndvdsadd  10538  infssuzcldc  10554  dfgcd2  10610  mulgcd  10612  ialgfx  10641  prmind2  10709  prm2orodd  10715  prmgt1  10720  oddprmgt2  10722  dfphi2  10803  evenennn  10813  bj-nfalt  10835  decidi  10865  sumdc2  10869  bdel  10903  bdssex  10960  bj-indind  10994  findset  11007
  Copyright terms: Public domain W3C validator