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  785  notnotrdc  787  pm2.61ddc  794  pm5.18dc  813  dcim  820  pm2.25dc  828  pm2.85dc  847  pm5.12dc  852  pm5.14dc  853  pm5.55dc  855  peircedc  856  pm5.54dc  863  dcor  879  pm5.62dc  889  pm5.63dc  890  pm4.83dc  895  3simpb  939  3simpc  940  3imp  1135  3com12  1145  3com13  1146  syl3anb  1215  xoranor  1311  xorbin  1318  xordc1  1327  biassdc  1329  nfr  1454  nfand  1503  19.21t  1517  19.30dc  1561  exintrbi  1567  19.9t  1576  nfnt  1589  equveli  1686  exdistrfor  1725  sbcof2  1735  sbidm  1776  sbi1v  1816  sbalyz  1920  sbal1yz  1922  nfsb4t  1935  euex  1975  eumo0  1976  mor  1987  exmodc  1995  mo3h  1998  mopick  2023  moexexdc  2029  euexex  2030  2euex  2032  exists2  2042  eqcoms  2088  eleq2s  2179  nfcr  2217  necon3ai  2300  rexnalim  2366  dfrex2dc  2367  rexex  2418  rsp  2419  ralim  2430  rexim  2463  r19.32r  2510  r19.44av  2522  r19.45av  2523  gencl  2645  gencbvex  2659  gencbval  2661  vtoclgf  2671  pm13.183  2745  elrabi  2759  eueq2dc  2779  eueq3dc  2780  mob2  2786  euxfr2dc  2791  reu3  2796  rmoim  2805  2rmorex  2810  sbcex  2837  sbcbi2  2878  ra5  2916  sseq1  3036  difdif  3114  dfss4st  3221  difindiss  3242  undif3ss  3249  dfrab3ss  3266  abvor0dc  3295  reldisj  3322  disjel  3325  inssdif0im  3338  uneqdifeqim  3355  r19.2m  3356  r19.3rm  3357  r19.9rmv  3360  rexm  3368  ralm  3373  raaanlem  3374  ifnefalse  3390  ifandc  3413  ifmdc  3414  nelpri  3455  nelprd  3457  prprc1  3535  difprsn2  3562  diftpsn3  3563  snsssn  3590  preqr2  3598  preq12b  3599  opthpr  3601  prneimg  3603  oprcl  3631  pwprss  3634  intmin4  3701  uniintabim  3710  dfiin2g  3748  iinss2  3767  iundif2ss  3780  invdisj  3817  trel  3920  trss  3922  ssex  3953  bnd2  3985  abssexg  3993  exmidexmid  4007  rext  4018  unipw  4020  euabex  4028  mss  4029  exss  4030  copsexg  4047  opelopabsb  4063  pwssunim  4087  epelg  4093  sowlin  4123  sotritric  4127  elsuci  4206  sucprc  4215  reusv3  4258  ordon  4278  onsucmin  4299  onsucelsucr  4300  unon  4303  onsucelsucexmid  4321  setind  4330  setind2  4331  sucprcreg  4340  en2lp  4345  eunex  4352  ordsoexmid  4353  ordpwsucss  4358  tfi  4372  peano1  4384  peano2  4385  find  4389  0nelelxp  4441  opelxp  4442  elvvuni  4472  optocl  4484  ralxpf  4552  rexxpf  4553  relop  4556  breldm  4610  dmxpm  4626  elreldm  4631  dmrnssfld  4666  dmcosseq  4674  resabs1  4711  resima2  4715  issref  4783  asymref  4786  xpidtr  4791  trin2  4792  poirr2  4793  xpmlem  4820  dmxpss  4829  xp11m  4837  cnveqb  4854  dfco2a  4899  cores2  4911  coi2  4915  relcnvtr  4918  relresfld  4928  relcnvexb  4938  cnviinm  4940  iotauni  4960  iota1  4962  iota4  4966  dffun8  5010  funcnvsn  5026  imadif  5061  imainlem  5062  fcoi1  5156  fcoi2  5157  f0rn0  5170  f1ocnv  5231  f1ocnvb  5232  fun11iun  5239  ffoss  5250  f1o00  5253  fo00  5254  relelfvdm  5301  nfvres  5302  nfunsn  5303  ssimaex  5330  fvmptss2  5344  fvmptssdm  5352  unpreima  5389  respreima  5392  elrnrexdm  5403  elrnrexdmb  5404  rexrnmpt  5407  dffo4  5412  rnmptss  5424  fvpr1  5464  fvpr2  5465  elunirn  5508  f1veqaeq  5511  isores1  5556  riotauni  5577  riotacl2  5584  riota1  5589  riota1a  5590  snriota  5600  eusvobj2  5601  acexmidlema  5606  acexmidlemb  5607  acexmidlem2  5612  oprabid  5640  0neqopab  5653  brabvv  5654  1stval2  5885  2ndval2  5886  xp1st  5895  xp2nd  5896  unielxp  5903  releldm2  5914  cnvf1o  5949  fo2ndf  5951  poxp  5956  reldmtpos  5974  dftpos4  5984  tpostpos  5985  tpostpos2  5986  iunon  6005  smoel  6021  tfrlem4  6034  tfrlem7  6038  tfrlem8  6039  tfrlem9  6040  nnaord  6222  ecexr  6251  swoord1  6275  swoord2  6276  0er  6280  mapprc  6363  mapsnconst  6405  idssen  6448  ener  6450  en0  6466  en1  6470  en1bg  6471  2dom  6476  enm  6490  xpsnen  6491  ssenen  6521  snnen2og  6529  php5dom  6533  phpm  6535  findcard  6558  findcard2  6559  findcard2s  6560  unfiexmid  6582  sbthlem1  6613  eldju2ndl  6710  eldju2ndr  6711  finnum  6758  exmidfodomrlemim  6774  indpi  6848  subhalfnqq  6920  archnqq  6923  enq0sym  6938  nqnq0pi  6944  nqnq0  6947  mulnnnq0  6956  prml  6983  prmu  6984  prssnql  6985  prssnqu  6986  prcdnql  6990  prcunqu  6991  prltlu  6993  prnmaxl  6994  prnminu  6995  prloc  6997  prdisj  6998  addcanprg  7122  recexprlemopl  7131  recexprlemopu  7133  cauappcvgprlemladdfu  7160  caucvgprlemladdfu  7183  recexgt0sr  7266  renfdisj  7493  negf1o  7807  recexre  7999  apsqgt0  8022  apreim  8024  recexaplem2  8063  rerecclap  8139  nn0ge0  8634  elnnnn0b  8653  xnn0xr  8677  xnn0nemnf  8683  xnn0nnn0pnf  8685  znegcl  8717  zeo  8787  nn0ind  8796  nn0ind-raph  8799  uzn0  8969  eluzaddi  8980  eluzsubi  8981  uznn0sub  8985  uz3m2nn  8996  uznnssnn  9000  uz2m1nn  9027  uz2mulcl  9030  indstr2  9031  qmulz  9043  qre  9045  qnegcl  9056  qreccl  9062  rphalflt  9098  nn0ledivnn  9173  xrltnr  9185  nltpnft  9214  ngtmnft  9215  xrrebnd  9216  xnegcl  9229  xnegneg  9230  xltnegi  9232  elioore  9265  elfzuz2  9378  uzsubsubfz  9396  fzdisj  9401  fzmmmeqm  9406  elfz0ubfz0  9467  elfz0fzfz0  9468  fz0fzelfz0  9469  fz0fzdiffz0  9472  elfzmlbp  9474  difelfzle  9476  difelfznle  9477  nn0disj  9480  2ffzeq  9483  fzo1fzo0n0  9525  elfzo0z  9526  elfzo0le  9527  fzonmapblen  9529  fzofzim  9530  elfzodifsumelfzo  9543  elfzonlteqm1  9552  fzonn0p1p1  9555  elfzom1p1elfzo  9556  ssfzo12bi  9567  ubmelm1fzo  9568  fzind2  9581  subfzo0  9584  rebtwn2z  9597  fldiv4p1lem1div2  9643  flqeqceilz  9656  zmodidfzoimp  9692  modfzo0difsn  9733  nnsinds  9780  nn0sinds  9781  expcl2lemap  9887  qexpclz  9896  facp1  10056  facnn2  10060  faclbnd3  10069  bcn1  10084  hashfz0  10151  cvg1nlemres  10335  rexanuz  10338  fclim  10598  climmo  10602  dvdsdivcl  10776  addmodlteqALT  10785  odd2np1  10798  oddge22np1  10806  m1expe  10824  nn0enne  10827  nn0o1gt2  10830  nno  10831  ndvdsadd  10856  infssuzcldc  10872  dfgcd2  10928  mulgcd  10930  ialgfx  10959  prmind2  11027  prm2orodd  11033  prmgt1  11038  oddprmgt2  11040  dfphi2  11121  evenennn  11131  bj-nfalt  11153  decidi  11183  sumdc2  11187  bdel  11224  bdssex  11281  bj-indind  11315  findset  11328  nninfall  11388
  Copyright terms: Public domain W3C validator