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  424  orcomd  635  3mix3  1061  ecase23d  1223  exlimdh  1465  nexd  1482  alexnim  1517  excomim  1531  19.41  1554  nfexd  1622  sbh  1637  sbcof2  1669  sbidm  1709  sb6rf  1711  nfsbt  1828  dvelimALT  1864  dvelimfv  1865  dvelimor  1872  eu2  1922  2euex  1965  eqcomd  2023  3eltr3g  2100  abbid  2132  neneqd  2201  syl5eqner  2210  3netr3g  2213  necomd  2265  r19.21bi  2381  nrexdv  2386  rexlimd  2404  rabbidva  2522  elisset  2541  euind  2701  rmoan  2712  reuind  2717  2rmorex  2718  spsbc  2748  spesbc  2816  eldifad  2902  eldifbd  2903  3sstr3g  2958  syl6sseq  2964  difindiss  3164  un00  3236  disjpss  3251  undifss  3276  disjpr2  3404  difprsn1  3473  diftpsn3  3475  difsnpssim  3477  difsnss  3480  sneqr  3501  preqr1  3509  preq12b  3511  oprcl  3543  intab  3614  riinm  3699  rintm  3714  sndisj  3730  3brtr3g  3765  trint  3839  iinexgm  3878  pwel  3924  exss  3933  0nelop  3955  euotd  3961  opelopabsb  3967  pwunim  3993  issod  4026  suctrALT  4103  orduniss  4108  onelini  4113  oneluni  4114  eusv2i  4133  rexxfrd  4141  rabxfrd  4147  reuhypd  4149  iunpw  4157  sucexg  4170  ordsucim  4172  ordtriexmidlem  4188  onsucelsucexmidlem  4194  ordsucunielexmid  4196  suc11g  4215  tfisi  4233  peano1  4240  peano2  4241  finds2  4247  brrelex12  4304  brel  4315  ssrel  4351  ssrel2  4353  ssrelrel  4363  elrel  4365  xpsspw  4373  relop  4409  dmxpm  4478  opelresi  4546  ndmima  4625  poirr2  4640  xpmlem  4667  xpimasn  4692  iotass  4807  iotacl  4813  funeu  4848  funeu2  4849  funopg  4856  funun  4866  funtp  4874  funcnvuni  4890  funcnvres2  4896  imadiflem  4900  imadif  4901  funimaexglem  4904  fneu2  4926  fnimaeq0  4942  fnmpt  4947  fun2  4985  f00  5002  foimacnv  5065  resdif  5069  f1ococnv1  5076  fv3  5118  relelfvdm  5126  nfvres  5127  dffn5im  5140  mptfvex  5177  fvmptdf  5179  fvmptdv2  5181  fndmdif  5193  dff4im  5234  fmpt  5240  fmptd  5243  f1oresrab  5250  fcoconst  5255  fsn  5256  ftpg  5268  fsnunf  5283  resfunexg  5303  isores1  5375  riota2df  5408  acexmidlemcase  5427  brabvv  5470  funoprabg  5519  fnovim  5528  ovmpt2df  5551  ovi3  5556  grprinvlem  5614  grprinvd  5615  grpridd  5616  elmpt2cl  5617  1stcof  5709  2ndcof  5710  fnmpt2  5747  fmpt2co  5756  fo2ndf  5767  f1o2ndf1  5768  brtpos2  5784  reldmtpos  5786  dftpos3  5795  dftpos4  5796  tpostpos2  5798  tposf2  5801  tposf12  5802  tposfo  5804  tposf  5805  smores2  5827  tfrlem1  5841  tfrlem3-2d  5846  tfrlemisucaccv  5856  tfrlemibxssdm  5858  tfrlemibfn  5859  tfrlemi1  5863  tfrexlem  5866  rdgivallem  5884  rdgisucinc  5888  rdgon  5889  frecabex  5895  frecfnom  5897  frecsuclemdm  5900  omsuc  5962  nntri2  5984  nnm00  6009  ecexr  6018  swoer  6041  elqsn0m  6081  iinerm  6085  erinxp  6087  ecinxp  6088  eroveu  6104  eroprf  6106  elni2  6168  distrnqg  6240  subhalfnqq  6265  enq0sym  6281  enq0ref  6282  enq0tr  6283  nqnq0pi  6287  nnnq0lem1  6295  distrnq0  6308  elinp  6322  elnp1st2nd  6324  prltlu  6335  prnmaxl  6336  prnminu  6337  prarloc  6351  nqprm  6391  appdivnq  6401  prmuloc  6404  mullocpr  6409  distrlem4prl  6417  distrlem4pru  6418  ltexprlemm  6431  ltexprlemopl  6432  ltexprlemopu  6434  prsrlem1  6483  gt0srpr  6489  ltresr  6544  bj-bdfindis  7308  bj-peano4  7316  strcollnfALT  7343  alsi1d  7351  alsi2d  7352  alsc1d  7353  alsc2d  7354
  Copyright terms: Public domain W3C validator