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  6525  appdivnq  6542  prmuloc  6545  mullocpr  6550  distrlem4prl  6558  distrlem4pru  6559  ltexprlemm  6572  ltexprlemopl  6573  ltexprlemopu  6575  prsrlem1  6630  gt0srpr  6636  ltresr  6696  nnind  7671  nn0supp  7970  nn0ge2m1nn  7978  zleloe  8028  zapne  8051  nn0lt2  8058  zindd  8092  uzm1  8239  uzin  8241  elnn1uz2  8280  nn01to3  8288  divfnzn  8292  qapne  8310  xrltnsym2  8445  iooval2  8514  icoshftf1o  8589  fztri3or  8633  fzneuz  8693  4fvwrd4  8727  elfzo0  8768  fzfig  8847  iseqovex  8859  iseqval  8860  expivallem  8870  expival  8871  expp1  8876  expcl2lemap  8881  expclzap  8894  expap0i  8901  bj-bdfindis  9335  bj-peano4  9343  strcollnfALT  9370  alsi1d  9378  alsi2d  9379  alsc1d  9380  alsc2d  9381
  Copyright terms: Public domain W3C validator