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

Theorem sylbi 120
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 119 . 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 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sylbb  122  sylbb2  137  3imtr4i  200  simplbiim  384  mpan10  465  an12s  554  an32s  557  an4s  577  sylnbi  667  dcim  826  notnotrdc  828  const  837  condcOLD  839  pm2.61ddc  846  pm5.18dc  868  pm2.25dc  878  pm2.85dc  890  pm5.12dc  895  pm5.14dc  896  pm5.55dc  898  peircedc  899  pm5.54dc  903  dcor  919  pm5.62dc  929  pm5.63dc  930  pm4.83dc  935  3simpb  979  3simpc  980  3imp  1175  3com12  1185  3com13  1186  syl3anb  1259  xoranor  1355  xorbin  1362  xordc1  1371  biassdc  1373  nfr  1498  nfand  1547  19.21t  1561  19.30dc  1606  exintrbi  1612  19.9t  1621  nfnt  1634  equveli  1732  exdistrfor  1772  sbcof2  1782  sbidm  1823  sbi1v  1863  sbalyz  1974  sbal1yz  1976  nfsb4t  1989  euex  2029  eumo0  2030  mor  2041  exmodc  2049  mo3h  2052  mopick  2077  moexexdc  2083  euexex  2084  2euex  2086  exists2  2096  eqcoms  2142  eleq2s  2234  nfcr  2273  necon3ai  2357  rexnalim  2427  dfrex2dc  2428  rexex  2479  rsp  2480  ralim  2491  rexim  2526  r19.32r  2578  r19.44av  2590  r19.45av  2591  gencl  2718  gencbvex  2732  gencbval  2734  vtoclgf  2744  vtoclg1f  2745  pm13.183  2822  elrabi  2837  eueq2dc  2857  eueq3dc  2858  mob2  2864  euxfr2dc  2869  reu3  2874  rmoim  2885  2rmorex  2890  sbcex  2917  sbcbi2  2959  ra5  2997  sseq1  3120  difdif  3201  dfss4st  3309  difindiss  3330  undif3ss  3337  dfrab3ss  3354  abvor0dc  3386  reldisj  3414  disjel  3417  inssdif0im  3430  uneqdifeqim  3448  r19.2m  3449  r19.2mOLD  3450  r19.3rm  3451  r19.9rmv  3454  rexm  3462  ralm  3467  raaanlem  3468  ifnefalse  3485  ifandc  3508  ifmdc  3509  nelpri  3551  nelprd  3553  prprc1  3631  difprsn2  3660  diftpsn3  3661  snsssn  3688  preqr2  3696  preq12b  3697  opthpr  3699  prneimg  3701  oprcl  3729  pwprss  3732  intmin4  3799  uniintabim  3808  dfiin2g  3846  iinss2  3865  iundif2ss  3878  disjnim  3920  disjnims  3921  invdisj  3923  disjiun  3924  brne0  3977  brm  3978  trel  4033  trss  4035  ssex  4065  bnd2  4097  abssexg  4106  exmidexmid  4120  rext  4137  unipw  4139  euabex  4147  mss  4148  exss  4149  copsexg  4166  opelopabsb  4182  pwssunim  4206  epelg  4212  sowlin  4242  sotritric  4246  elsuci  4325  sucprc  4334  reusv3  4381  ordon  4402  onsucmin  4423  onsucelsucr  4424  unon  4427  onsucelsucexmid  4445  setind  4454  setind2  4455  sucprcreg  4464  en2lp  4469  eunex  4476  ordsoexmid  4477  ordpwsucss  4482  tfi  4496  peano1  4508  peano2  4509  find  4513  0nelelxp  4568  opelxp  4569  elvvuni  4603  optocl  4615  ralxpf  4685  rexxpf  4686  relop  4689  breldm  4743  dmxpm  4759  elreldm  4765  dmrnssfld  4802  dmcosseq  4810  resabs1  4848  resima2  4853  issref  4921  asymref  4924  xpidtr  4929  trin2  4930  poirr2  4931  xpmlem  4959  dmxpss  4969  xp11m  4977  cnveqb  4994  dfco2a  5039  cores2  5051  coi2  5055  relcnvtr  5058  relresfld  5068  relcnvexb  5078  cnviinm  5080  iotauni  5100  iota1  5102  iota4  5106  dffun8  5151  funcnvsn  5168  imadif  5203  imainlem  5204  fcoi1  5303  fcoi2  5304  f0rn0  5317  f1ocnv  5380  f1ocnvb  5381  fun11iun  5388  ffoss  5399  f1o00  5402  fo00  5403  relelfvdm  5453  nfvres  5454  nfunsn  5455  ssimaex  5482  fvmptss2  5496  fvmptssdm  5505  unpreima  5545  respreima  5548  elrnrexdm  5559  elrnrexdmb  5560  rexrnmpt  5563  dffo4  5568  rnmptss  5581  fvpr1  5624  fvpr2  5625  elunirn  5667  f1veqaeq  5670  isores1  5715  riotauni  5736  riotacl2  5743  riota1  5748  riota1a  5749  snriota  5759  eusvobj2  5760  acexmidlema  5765  acexmidlemb  5766  acexmidlem2  5771  oprabid  5803  0neqopab  5816  brabvv  5817  1stval2  6053  2ndval2  6054  xp1st  6063  xp2nd  6064  unielxp  6072  releldm2  6083  cnvf1o  6122  fo2ndf  6124  poxp  6129  reldmtpos  6150  dftpos4  6160  tpostpos  6161  tpostpos2  6162  iunon  6181  smoel  6197  tfrlem4  6210  tfrlem7  6214  tfrlem8  6215  tfrlem9  6216  nnaord  6405  ecexr  6434  swoord1  6458  swoord2  6459  0er  6463  mapprc  6546  mapsnconst  6588  ixpf  6614  mptelixpg  6628  idssen  6671  ener  6673  en0  6689  en1  6693  en1bg  6694  2dom  6699  enm  6714  xpsnen  6715  ssenen  6745  snnen2og  6753  php5dom  6757  phpm  6759  findcard  6782  findcard2  6783  findcard2s  6784  unfiexmid  6806  fiintim  6817  fidcenumlemim  6840  sbthlem1  6845  fiss  6865  djuexb  6929  djuss  6955  eldju2ndl  6957  eldju2ndr  6958  ctssdclemr  6997  exmidlpo  7015  finnum  7044  exmidfodomrlemim  7062  indpi  7162  subhalfnqq  7234  archnqq  7237  enq0sym  7252  nqnq0pi  7258  nqnq0  7261  mulnnnq0  7270  prml  7297  prmu  7298  prssnql  7299  prssnqu  7300  prcdnql  7304  prcunqu  7305  prltlu  7307  prnmaxl  7308  prnminu  7309  prloc  7311  prdisj  7312  addcanprg  7436  recexprlemopl  7445  recexprlemopu  7447  cauappcvgprlemladdfu  7474  caucvgprlemladdfu  7497  recexgt0sr  7593  renfdisj  7836  axsuploc  7849  negf1o  8156  recexre  8352  apsqgt0  8375  apreim  8377  aprcl  8420  recexaplem2  8425  rerecclap  8502  nn0ge0  9014  elnnnn0b  9033  xnn0xr  9057  xnn0nemnf  9063  xnn0nnn0pnf  9065  znegcl  9097  zeo  9168  nn0ind  9177  nn0ind-raph  9180  uzn0  9353  eluzaddi  9364  eluzsubi  9365  uznn0sub  9369  uz3m2nn  9380  uznnssnn  9384  uz2m1nn  9411  uz2mulcl  9414  indstr2  9415  qmulz  9427  qre  9429  qnegcl  9440  qreccl  9446  rphalflt  9483  nn0ledivnn  9566  xrltnr  9578  nltpnft  9609  ngtmnft  9612  xrrebnd  9614  xnegcl  9627  xnegneg  9628  xltnegi  9630  xrpnfdc  9637  xrmnfdc  9638  xnegid  9654  xaddid1  9657  xnn0lenn0nn0  9660  xnn0xadd0  9662  xposdif  9677  elioore  9707  elfzuz2  9821  uzsubsubfz  9839  fzdisj  9844  fzmmmeqm  9850  elfz0ubfz0  9914  elfz0fzfz0  9915  fz0fzelfz0  9916  fz0fzdiffz0  9919  elfzmlbp  9921  difelfzle  9923  difelfznle  9924  nn0disj  9927  2ffzeq  9930  fzo1fzo0n0  9972  elfzo0z  9973  elfzo0le  9974  fzonmapblen  9976  fzofzim  9977  elfzodifsumelfzo  9990  elfzonlteqm1  9999  fzonn0p1p1  10002  elfzom1p1elfzo  10003  ssfzo12bi  10014  ubmelm1fzo  10015  fzind2  10028  subfzo0  10031  rebtwn2z  10044  fldiv4p1lem1div2  10090  flqeqceilz  10103  zmodidfzoimp  10139  modfzo0difsn  10180  nnsinds  10228  nn0sinds  10229  expcl2lemap  10317  qexpclz  10326  facp1  10488  facnn2  10492  faclbnd3  10501  bcn1  10516  hashfz0  10583  cvg1nlemres  10769  rexanuz  10772  fclim  11075  climmo  11079  iser3shft  11127  fsumsplitsn  11191  fsum2dlemstep  11215  fisumcom2  11219  arisum  11279  arisum2  11280  prodmodc  11359  eftlub  11408  ef01bndlem  11474  sin01gt0  11479  cos01gt0  11480  sin02gt0  11481  dvdsdivcl  11559  addmodlteqALT  11568  odd2np1  11581  oddge22np1  11589  m1expe  11607  nn0enne  11610  nn0o1gt2  11613  nno  11614  ndvdsadd  11639  infssuzcldc  11655  dfgcd2  11713  mulgcd  11715  algfx  11744  prmind2  11812  prm2orodd  11818  prmgt1  11823  oddprmgt2  11825  dfphi2  11907  evenennn  11917  distop  12268  ntrss  12302  ssntr  12305  lmrcl  12374  lmreltop  12376  txuni2  12439  txcn  12458  hmeocnvb  12501  xmetunirn  12541  blssioo  12728  divcnap  12738  cdivcncfap  12770  dedekindeulemlub  12781  dedekindicclemlub  12790  dvexp2  12859  pilem3  12886  sincosq1sgn  12929  sincosq2sgn  12930  sincosq3sgn  12931  sincosq4sgn  12932  sinq12gt0  12933  bj-pm2.18st  13042  bj-dcstab  13045  decidi  13086  sumdc2  13090  bdel  13127  bdssex  13184  bj-indind  13214  findset  13227  nninfall  13290  trirec0  13323
  Copyright terms: Public domain W3C validator