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

Theorem sylib 127
Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
sylib.1 (φψ)
sylib.2 (ψχ)
Assertion
Ref Expression
sylib (φχ)

Proof of Theorem sylib
StepHypRef Expression
1 sylib.1 . 2 (φψ)
2 sylib.2 . . 3 (ψχ)
32biimpi 113 . 2 (ψχ)
41, 3syl 14 1 (φχ)
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:  bicomd  129  pm5.74d  171  bitri  173  3imtr3i  189  ancomd  254  pm4.71d  373  pm4.71rd  374  imdistand  421  orcomd  647  3mix3  1074  mpjao3dan  1201  ecase23d  1239  exlimdh  1484  nexd  1501  alexnim  1536  excomim  1550  19.41  1573  nfexd  1641  sbh  1656  sbcof2  1688  sbidm  1728  sb6rf  1730  nfsbt  1847  dvelimALT  1883  dvelimfv  1884  dvelimor  1891  eu2  1941  2euex  1984  eqcomd  2042  3eltr3g  2119  abbid  2151  neneqd  2221  syl5eqner  2230  3netr3g  2233  necomd  2285  r19.21bi  2401  nrexdv  2406  rexlimd  2424  rabbidva  2542  elisset  2562  euind  2722  rmoan  2733  reuind  2738  2rmorex  2739  spsbc  2769  spesbc  2837  eldifad  2923  eldifbd  2924  3sstr3g  2979  syl6sseq  2985  difindiss  3185  un00  3257  disjpss  3272  undifss  3297  disjpr2  3425  difprsn1  3494  diftpsn3  3496  difsnpssim  3498  difsnss  3501  sneqr  3522  preqr1  3530  preq12b  3532  oprcl  3564  intab  3635  riinm  3720  rintm  3735  sndisj  3751  3brtr3g  3786  trint  3860  iinexgm  3899  pwel  3945  exss  3954  0nelop  3976  euotd  3982  opelopabsb  3988  pwunim  4014  issod  4047  suctr  4124  orduniss  4128  onelini  4133  oneluni  4134  eusv2i  4153  rexxfrd  4161  rabxfrd  4167  reuhypd  4169  iunpw  4177  sucexg  4190  ordsucim  4192  ordtriexmidlem  4208  onsucelsucexmidlem  4214  ordsucunielexmid  4216  suc11g  4235  tfisi  4253  peano1  4260  peano2  4261  finds2  4267  brrelex12  4324  brel  4335  ssrel  4371  ssrel2  4373  ssrelrel  4383  elrel  4385  xpsspw  4393  relop  4429  dmxpm  4498  opelresi  4566  ndmima  4645  poirr2  4660  xpmlem  4687  xpimasn  4712  iotass  4827  iotacl  4833  dffun5r  4857  funeu  4869  funeu2  4870  funopg  4877  funun  4887  funtp  4895  funcnvuni  4911  funcnvres2  4917  imadiflem  4921  imadif  4922  funimaexglem  4925  fneu2  4947  fnimaeq0  4963  fnmpt  4968  fun2  5007  f00  5024  foimacnv  5087  resdif  5091  f1ococnv1  5098  fv3  5140  relelfvdm  5148  nfvres  5149  dffn5im  5162  mptfvex  5199  fvmptdf  5201  fvmptdv2  5203  fndmdif  5215  dff4im  5256  fmpt  5262  fmptd  5265  f1oresrab  5272  fcoconst  5277  fsn  5278  ftpg  5290  fsnunf  5305  resfunexg  5325  isores1  5397  riota2df  5431  acexmidlemcase  5450  brabvv  5493  funoprabg  5542  fnovim  5551  ovmpt2df  5574  ovi3  5579  grprinvlem  5637  grprinvd  5638  grpridd  5639  elmpt2cl  5640  1stcof  5732  2ndcof  5733  fnmpt2  5770  fmpt2co  5779  fo2ndf  5790  f1o2ndf1  5791  brtpos2  5807  reldmtpos  5809  dftpos3  5818  dftpos4  5819  tpostpos2  5821  tposf2  5824  tposf12  5825  tposfo  5827  tposf  5828  smores2  5850  tfrlem1  5864  tfrlem3-2d  5869  tfrlemisucaccv  5880  tfrlemibxssdm  5882  tfrlemibfn  5883  tfrlemi1  5887  tfrexlem  5889  rdgivallem  5908  rdgisucinc  5912  rdgon  5913  frecabex  5923  frecfnom  5925  frecsuclemdm  5927  freccl  5932  omsuc  5990  nntri2  6012  nnm00  6038  ecexr  6047  swoer  6070  elqsn0m  6110  iinerm  6114  erinxp  6116  ecinxp  6117  eroveu  6133  eroprf  6135  dom2lem  6188  fundmen  6222  ssfiexmid  6254  elni2  6298  indpi  6326  distrnqg  6371  subhalfnqq  6397  enq0sym  6415  enq0ref  6416  enq0tr  6417  nqnq0pi  6421  nnnq0lem1  6429  distrnq0  6442  elinp  6457  elnp1st2nd  6459  prltlu  6470  prnmaxl  6471  prnminu  6472  prarloc  6486  nqprm  6525  appdivnq  6544  prmuloc  6547  mullocpr  6552  distrlem4prl  6560  distrlem4pru  6561  ltexprlemm  6574  ltexprlemopl  6575  ltexprlemopu  6577  cauappcvgprlemopl  6618  cauappcvgprlemopu  6620  cauappcvgprlemdisj  6623  cauappcvgprlem2  6632  cauappcvgprlemlim  6633  caucvgprlemnkj  6637  caucvgprlemopl  6640  caucvgprlemopu  6642  caucvgprlemdisj  6645  caucvgprlemcl  6647  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlem2  6651  prsrlem1  6670  gt0srpr  6676  ltresr  6736  nnind  7711  nn0supp  8010  nn0ge2m1nn  8018  zleloe  8068  zapne  8091  nn0lt2  8098  zindd  8132  uzm1  8279  uzin  8281  elnn1uz2  8320  nn01to3  8328  divfnzn  8332  qapne  8350  xrltnsym2  8485  iooval2  8554  icoshftf1o  8629  fztri3or  8673  fzneuz  8733  4fvwrd4  8767  elfzo0  8808  fzfig  8887  iseqovex  8899  iseqval  8900  expivallem  8910  expival  8911  expp1  8916  expcl2lemap  8921  expclzap  8934  expap0i  8941  bj-bdfindis  9407  bj-peano4  9415  strcollnfALT  9446  alsi1d  9454  alsi2d  9455  alsc1d  9456  alsc2d  9457
  Copyright terms: Public domain W3C validator