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  6414  enq0ref  6415  enq0tr  6416  nqnq0pi  6420  nnnq0lem1  6428  distrnq0  6441  elinp  6456  elnp1st2nd  6458  prltlu  6469  prnmaxl  6470  prnminu  6471  prarloc  6485  nqprm  6524  appdivnq  6543  prmuloc  6546  mullocpr  6551  distrlem4prl  6559  distrlem4pru  6560  ltexprlemm  6573  ltexprlemopl  6574  ltexprlemopu  6576  cauappcvgprlemopl  6617  cauappcvgprlemopu  6619  cauappcvgprlemdisj  6622  cauappcvgprlem2  6631  cauappcvgprlemlim  6632  prsrlem1  6650  gt0srpr  6656  ltresr  6716  nnind  7691  nn0supp  7990  nn0ge2m1nn  7998  zleloe  8048  zapne  8071  nn0lt2  8078  zindd  8112  uzm1  8259  uzin  8261  elnn1uz2  8300  nn01to3  8308  divfnzn  8312  qapne  8330  xrltnsym2  8465  iooval2  8534  icoshftf1o  8609  fztri3or  8653  fzneuz  8713  4fvwrd4  8747  elfzo0  8788  fzfig  8867  iseqovex  8879  iseqval  8880  expivallem  8890  expival  8891  expp1  8896  expcl2lemap  8901  expclzap  8914  expap0i  8921  bj-bdfindis  9381  bj-peano4  9389  strcollnfALT  9416  alsi1d  9424  alsi2d  9425  alsc1d  9426  alsc2d  9427
  Copyright terms: Public domain W3C validator