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

Theorem sylib 131
Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
sylib.1  |-  ( ph  ->  ps )
sylib.2  |-  ( ps  <->  ch )
Assertion
Ref Expression
sylib  |-  ( ph  ->  ch )

Proof of Theorem sylib
StepHypRef Expression
1 sylib.1 . 2  |-  ( ph  ->  ps )
2 sylib.2 . . 3  |-  ( ps  <->  ch )
32biimpi 117 . 2  |-  ( ps 
->  ch )
41, 3syl 14 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  bicomd  133  pm5.74d  175  bitri  177  3imtr3i  193  ancomd  258  pm4.71d  379  pm4.71rd  380  imdistand  429  orcomd  658  3mix3  1086  mpjao3dan  1213  ecase23d  1256  exlimdh  1503  nexd  1520  alexnim  1555  excomim  1569  19.41  1592  nfexd  1660  sbh  1675  sbcof2  1707  sbidm  1747  sb6rf  1749  nfsbt  1866  dvelimALT  1902  dvelimfv  1903  dvelimor  1910  eu2  1960  2euex  2003  eqcomd  2061  3eltr3g  2138  abbid  2170  neneqd  2241  syl5eqner  2251  3netr3g  2254  necomd  2306  r19.21bi  2424  nrexdv  2429  rexlimd  2447  rabbidva  2565  elisset  2585  euind  2751  rmoan  2762  reuind  2767  2rmorex  2768  spsbc  2798  spesbc  2871  eldifad  2957  eldifbd  2958  3sstr3g  3013  syl6sseq  3019  difindiss  3219  un00  3291  disjpss  3306  undifss  3331  ifcldcd  3386  disjpr2  3462  difprsn1  3531  diftpsn3  3533  difsnpssim  3535  difsnss  3538  sneqr  3559  preqr1  3567  preq12b  3569  oprcl  3601  intab  3672  riinm  3757  rintm  3772  sndisj  3788  3brtr3g  3823  trint  3897  iinexgm  3936  pwel  3982  exss  3991  0nelop  4013  euotd  4019  opelopabsb  4025  pwunim  4051  issod  4084  frind  4117  suctr  4186  orduniss  4190  onelini  4195  oneluni  4196  eusv2i  4215  rexxfrd  4223  rabxfrd  4229  reuhypd  4231  iunpw  4239  sucexg  4252  ordsucim  4254  ordtriexmidlem  4273  ordtri2or2exmidlem  4279  onsucelsucexmidlem  4282  ordsucunielexmid  4284  orddif  4299  suc11g  4309  onintexmid  4325  reg3exmidlemwe  4331  tfisi  4338  peano1  4345  peano2  4346  finds2  4352  brrelex12  4409  brel  4420  ssrel  4456  ssrel2  4458  ssrelrel  4468  elrel  4470  xpsspw  4478  relop  4514  dmxpm  4583  opelresi  4651  ndmima  4730  poirr2  4745  xpmlem  4772  xpimasn  4797  iotass  4912  iotacl  4918  dffun5r  4942  funeu  4954  funeu2  4955  funopg  4962  funun  4972  funtp  4980  funcnvuni  4996  funcnvres2  5002  imadiflem  5006  imadif  5007  funimaexglem  5010  fneu2  5032  fnimaeq0  5048  fnmpt  5053  fun2  5092  f00  5109  foimacnv  5172  resdif  5176  f1ococnv1  5183  fv3  5225  relelfvdm  5233  nfvres  5234  dffn5im  5247  mptfvex  5284  fvmptdf  5286  fvmptdv2  5288  fndmdif  5300  dff4im  5341  fmpt  5347  fmptd  5350  f1oresrab  5357  fcoconst  5362  fsn  5363  ftpg  5375  fsnunf  5390  resfunexg  5410  isores1  5482  riota2df  5516  acexmidlemcase  5535  brabvv  5579  funoprabg  5628  fnovim  5637  ovmpt2df  5660  ovi3  5665  grprinvlem  5723  grprinvd  5724  grpridd  5725  elmpt2cl  5726  1stcof  5818  2ndcof  5819  fnmpt2  5856  fmpt2co  5865  fo2ndf  5876  f1o2ndf1  5877  brtpos2  5897  reldmtpos  5899  dftpos3  5908  dftpos4  5909  tpostpos2  5911  tposf2  5914  tposf12  5915  tposfo  5917  tposf  5918  smores2  5940  tfrlem1  5954  tfrlem3-2d  5959  tfrlemisucaccv  5970  tfrlemibxssdm  5972  tfrlemibfn  5973  tfrlemi1  5977  tfrexlem  5979  rdgivallem  5999  rdgisucinc  6003  rdgon  6004  frecabex  6015  frecfnom  6017  frecsuclemdm  6019  freccl  6024  omsuc  6082  nntri2  6104  nnsseleq  6110  nndifsnid  6111  nnm00  6133  ecexr  6142  swoer  6165  elqsn0m  6205  iinerm  6209  erinxp  6211  ecinxp  6212  eroveu  6228  eroprf  6230  dom2lem  6283  fundmen  6317  nneneq  6351  fidifsnid  6363  ssfiexmid  6367  dif1en  6368  fin0  6373  fin0or  6374  diffitest  6375  diffisn  6381  ac6sfi  6383  onunsnss  6386  suplubti  6406  elni2  6470  indpi  6498  distrnqg  6543  subhalfnqq  6570  enq0sym  6588  enq0ref  6589  enq0tr  6590  nqnq0pi  6594  nnnq0lem1  6602  distrnq0  6615  elinp  6630  elnp1st2nd  6632  prltlu  6643  prnmaxl  6644  prnminu  6645  prarloc  6659  nqprm  6698  appdivnq  6719  prmuloc  6722  mullocpr  6727  distrlem4prl  6740  distrlem4pru  6741  ltexprlemm  6756  ltexprlemopl  6757  ltexprlemopu  6759  cauappcvgprlemopl  6802  cauappcvgprlemopu  6804  cauappcvgprlemdisj  6807  cauappcvgprlem2  6816  cauappcvgprlemlim  6817  caucvgprlemnkj  6822  caucvgprlemopl  6825  caucvgprlemopu  6827  caucvgprlemdisj  6830  caucvgprlemcl  6832  caucvgprlemladdfu  6833  caucvgprlemladdrl  6834  caucvgprlem2  6836  caucvgprprlemcbv  6843  caucvgprprlemval  6844  caucvgprprlemlol  6854  caucvgprprlemexbt  6862  caucvgprprlem1  6865  prsrlem1  6885  gt0srpr  6891  caucvgsrlemcl  6931  caucvgsrlembound  6936  caucvgsrlemgt1  6937  ltresr  6973  nnindnn  7025  axcaucvglemcl  7027  axcaucvglemval  7029  axcaucvglemcau  7030  axcaucvglemres  7031  nnind  8006  nn0supp  8291  nn0ge2m1nn  8299  zleloe  8349  zapne  8373  nn0lt2  8380  zindd  8415  uzm1  8599  uzin  8601  elnn1uz2  8641  nn01to3  8649  divfnzn  8653  qapne  8671  xrltnsym2  8816  iooval2  8885  icoshftf1o  8960  fztri3or  9005  fzneuz  9065  4fvwrd4  9099  elfzo0  9140  ioom  9217  fzfig  9370  iseqovex  9383  iseqval  9384  monoord2  9400  iseqdistr  9414  expivallem  9421  expival  9422  expp1  9427  expcl2lemap  9432  expclzap  9445  expap0i  9452  ibcval5  9631  cvg1nlemcau  9811  rexanuz  9815  resqrexlemoverl  9848  resqrexlemglsq  9849  resqrexlemsqa  9851  resqrexlemex  9852  rersqreu  9855  caubnd2  9944  climreu  10049  iiserex  10090  climcvg1nlem  10099  serif0  10102  mod2eq1n2dvds  10191  ndvdssub  10242  nn0seqcvgd  10263  bj-bdfindis  10459  bj-peano4  10467  strcollnfALT  10498  alsi1d  10507  alsi2d  10508  alsc1d  10509  alsc2d  10510
  Copyright terms: Public domain W3C validator