ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylib 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  648  3mix3  1075  mpjao3dan  1202  ecase23d  1240  exlimdh  1487  nexd  1504  alexnim  1539  excomim  1553  19.41  1576  nfexd  1644  sbh  1659  sbcof2  1691  sbidm  1731  sb6rf  1733  nfsbt  1850  dvelimALT  1886  dvelimfv  1887  dvelimor  1894  eu2  1944  2euex  1987  eqcomd  2045  3eltr3g  2122  abbid  2154  neneqd  2226  syl5eqner  2236  3netr3g  2239  necomd  2291  r19.21bi  2407  nrexdv  2412  rexlimd  2430  rabbidva  2548  elisset  2568  euind  2728  rmoan  2739  reuind  2744  2rmorex  2745  spsbc  2775  spesbc  2843  eldifad  2929  eldifbd  2930  3sstr3g  2985  syl6sseq  2991  difindiss  3191  un00  3263  disjpss  3278  undifss  3303  ifcldcd  3358  disjpr2  3434  difprsn1  3503  diftpsn3  3505  difsnpssim  3507  difsnss  3510  sneqr  3531  preqr1  3539  preq12b  3541  oprcl  3573  intab  3644  riinm  3729  rintm  3744  sndisj  3760  3brtr3g  3795  trint  3869  iinexgm  3908  pwel  3954  exss  3963  0nelop  3985  euotd  3991  opelopabsb  3997  pwunim  4023  issod  4056  frind  4089  suctr  4158  orduniss  4162  onelini  4167  oneluni  4168  eusv2i  4187  rexxfrd  4195  rabxfrd  4201  reuhypd  4203  iunpw  4211  sucexg  4224  ordsucim  4226  ordtriexmidlem  4245  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  ordsucunielexmid  4256  orddif  4271  suc11g  4281  onintexmid  4297  reg3exmidlemwe  4303  tfisi  4310  peano1  4317  peano2  4318  finds2  4324  brrelex12  4381  brel  4392  ssrel  4428  ssrel2  4430  ssrelrel  4440  elrel  4442  xpsspw  4450  relop  4486  dmxpm  4555  opelresi  4623  ndmima  4702  poirr2  4717  xpmlem  4744  xpimasn  4769  iotass  4884  iotacl  4890  dffun5r  4914  funeu  4926  funeu2  4927  funopg  4934  funun  4944  funtp  4952  funcnvuni  4968  funcnvres2  4974  imadiflem  4978  imadif  4979  funimaexglem  4982  fneu2  5004  fnimaeq0  5020  fnmpt  5025  fun2  5064  f00  5081  foimacnv  5144  resdif  5148  f1ococnv1  5155  fv3  5197  relelfvdm  5205  nfvres  5206  dffn5im  5219  mptfvex  5256  fvmptdf  5258  fvmptdv2  5260  fndmdif  5272  dff4im  5313  fmpt  5319  fmptd  5322  f1oresrab  5329  fcoconst  5334  fsn  5335  ftpg  5347  fsnunf  5362  resfunexg  5382  isores1  5454  riota2df  5488  acexmidlemcase  5507  brabvv  5551  funoprabg  5600  fnovim  5609  ovmpt2df  5632  ovi3  5637  grprinvlem  5695  grprinvd  5696  grpridd  5697  elmpt2cl  5698  1stcof  5790  2ndcof  5791  fnmpt2  5828  fmpt2co  5837  fo2ndf  5848  f1o2ndf1  5849  brtpos2  5866  reldmtpos  5868  dftpos3  5877  dftpos4  5878  tpostpos2  5880  tposf2  5883  tposf12  5884  tposfo  5886  tposf  5887  smores2  5909  tfrlem1  5923  tfrlem3-2d  5928  tfrlemisucaccv  5939  tfrlemibxssdm  5941  tfrlemibfn  5942  tfrlemi1  5946  tfrexlem  5948  rdgivallem  5968  rdgisucinc  5972  rdgon  5973  frecabex  5984  frecfnom  5986  frecsuclemdm  5988  freccl  5993  omsuc  6051  nntri2  6073  nnsseleq  6079  nndifsnid  6080  nnm00  6102  ecexr  6111  swoer  6134  elqsn0m  6174  iinerm  6178  erinxp  6180  ecinxp  6181  eroveu  6197  eroprf  6199  dom2lem  6252  fundmen  6286  nneneq  6320  fidifsnid  6332  ssfiexmid  6336  dif1en  6337  fin0  6342  fin0or  6343  diffitest  6344  diffisn  6350  ac6sfi  6352  elni2  6410  indpi  6438  distrnqg  6483  subhalfnqq  6510  enq0sym  6528  enq0ref  6529  enq0tr  6530  nqnq0pi  6534  nnnq0lem1  6542  distrnq0  6555  elinp  6570  elnp1st2nd  6572  prltlu  6583  prnmaxl  6584  prnminu  6585  prarloc  6599  nqprm  6638  appdivnq  6659  prmuloc  6662  mullocpr  6667  distrlem4prl  6680  distrlem4pru  6681  ltexprlemm  6696  ltexprlemopl  6697  ltexprlemopu  6699  cauappcvgprlemopl  6742  cauappcvgprlemopu  6744  cauappcvgprlemdisj  6747  cauappcvgprlem2  6756  cauappcvgprlemlim  6757  caucvgprlemnkj  6762  caucvgprlemopl  6765  caucvgprlemopu  6767  caucvgprlemdisj  6770  caucvgprlemcl  6772  caucvgprlemladdfu  6773  caucvgprlemladdrl  6774  caucvgprlem2  6776  caucvgprprlemcbv  6783  caucvgprprlemval  6784  caucvgprprlemlol  6794  caucvgprprlemexbt  6802  caucvgprprlem1  6805  prsrlem1  6825  gt0srpr  6831  caucvgsrlemcl  6871  caucvgsrlembound  6876  caucvgsrlemgt1  6877  ltresr  6913  nnindnn  6965  axcaucvglemcl  6967  axcaucvglemval  6969  axcaucvglemcau  6970  axcaucvglemres  6971  nnind  7928  nn0supp  8232  nn0ge2m1nn  8240  zleloe  8290  zapne  8313  nn0lt2  8320  zindd  8354  uzm1  8501  uzin  8503  elnn1uz2  8542  nn01to3  8550  divfnzn  8554  qapne  8572  xrltnsym2  8713  iooval2  8782  icoshftf1o  8857  fztri3or  8901  fzneuz  8961  4fvwrd4  8995  elfzo0  9036  fzfig  9180  iseqovex  9193  iseqval  9194  monoord2  9210  iseqdistr  9223  expivallem  9230  expival  9231  expp1  9236  expcl2lemap  9241  expclzap  9254  expap0i  9261  cvg1nlemcau  9557  rexanuz  9561  resqrexlemoverl  9593  resqrexlemglsq  9594  resqrexlemsqa  9596  resqrexlemex  9597  rersqreu  9600  caubnd2  9687  climreu  9792  iiserex  9833  climcvg1nlem  9842  serif0  9845  nn0seqcvgd  9854  bj-bdfindis  10046  bj-peano4  10054  strcollnfALT  10085  alsi1d  10093  alsi2d  10094  alsc1d  10095  alsc2d  10096
  Copyright terms: Public domain W3C validator