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  6416  addclnq0  6433  mulclnq0  6434  nq0m0r  6438  prarloclemlo  6476  prarloc  6485  genpml  6499  genpmu  6500  addnqprl  6511  addnqpru  6512  prmuloc2  6547  1idpru  6566  ltexprlemm  6573  ltexprlemloc  6580  recexprlemm  6595  recexprlem1ssl  6604  addclsr  6661  mulclsr  6662  mulap0r  7379  nn1suc  7694  prime  8093  zindd  8112  xrlttri3  8468  fzopth  8674  fzsuc  8681  fzpred  8682  fzp1ss  8685  fztp  8690  fseq1p1m1  8706  1fv  8746  elfzom1elp1fzo  8808  ssfzo12  8830  fzosplitsn  8839  frecuzrdgcl  8860  frecuzrdgsuc  8862  frecfzennn  8864  frecfzen2  8865  cjcj  9091  bj-inex  9338  bj-sucexg  9353  bj-peano4  9389  setindis  9397  bdsetindis  9399  bj-inf2vnlem1  9400
  Copyright terms: Public domain W3C validator