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

Theorem 3syl 17
Description: Inference chaining two syllogisms. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3syl.1 (φψ)
3syl.2 (ψχ)
3syl.3 (χθ)
Assertion
Ref Expression
3syl (φθ)

Proof of Theorem 3syl
StepHypRef Expression
1 3syl.1 . . 3 (φψ)
2 3syl.2 . . 3 (ψχ)
31, 2syl 14 . 2 (φχ)
4 3syl.3 . 2 (χθ)
53, 4syl 14 1 (φθ)
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  4syl  18  hbim  1434  19.9hd  1549  equsexd  1614  sbcof2  1688  aev  1690  sbequi  1717  nfsbd  1848  mo2n  1925  eupickb  1978  r19.29af2  2446  spc2gv  2637  spc3gv  2639  eqvincg  2662  sbcco3g  2897  snelpwi  3939  opth1  3964  onin  4089  reusv1  4156  xpexg  4395  dmexg  4539  rnexg  4540  relfld  4789  funimaexglem  4925  funimaexg  4926  fabexg  5020  nfvres  5149  funimass4  5167  funconstss  5228  f1oresrab  5272  resfunexg  5325  f1eqcocnv  5374  isores1  5397  isoini  5400  isose  5403  isopolem  5404  isosolem  5406  eusvobj2  5441  acexmidlemcase  5450  oprabid  5480  offval  5661  resfunexgALT  5679  offval3  5703  1stvalg  5711  2ndvalg  5712  1stcof  5732  2ndcof  5733  cnvf1o  5788  tposf12  5825  smores3  5849  smoiso  5858  tfr0  5878  tfrlemibxssdm  5882  tfrlemi14d  5888  tfrexlem  5889  rdgss  5910  frecsuclemdm  5927  nnsucsssuc  6010  swoord1  6071  swoord2  6072  iinerm  6114  eroveu  6133  en1uniel  6220  fopwdom  6246  addclnq  6359  mulclnq  6360  1qec  6372  prarloclemarch2  6402  enq0tr  6417  addclnq0  6434  mulclnq0  6435  nq0m0r  6439  prarloclemlo  6477  prarloc  6486  genpml  6500  genpmu  6501  addnqprl  6512  addnqpru  6513  prmuloc2  6548  1idpru  6567  ltexprlemm  6574  ltexprlemloc  6581  recexprlemm  6596  recexprlem1ssl  6605  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemlol  6641  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  addclsr  6681  mulclsr  6682  mulap0r  7399  nn1suc  7714  prime  8113  zindd  8132  xrlttri3  8488  fzopth  8694  fzsuc  8701  fzpred  8702  fzp1ss  8705  fztp  8710  fseq1p1m1  8726  1fv  8766  elfzom1elp1fzo  8828  ssfzo12  8850  fzosplitsn  8859  frecuzrdgcl  8880  frecuzrdgsuc  8882  frecfzennn  8884  frecfzen2  8885  cjcj  9111  bj-inex  9362  bj-sucexg  9377  bj-peano4  9415  setindis  9427  bdsetindis  9429  bj-inf2vnlem1  9430
  Copyright terms: Public domain W3C validator