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  1410  19.9hd  1525  equsexd  1590  sbcof2  1664  aev  1666  sbequi  1693  nfsbd  1824  mo2n  1901  eupickb  1954  r19.29af2  2421  spc2gv  2611  spc3gv  2613  eqvincg  2636  sbcco3g  2871  snelpwi  3911  opth1  3936  onin  4061  reusv1  4128  xpexg  4367  dmexg  4511  rnexg  4512  relfld  4761  funimaexglem  4896  funimaexg  4897  fabexg  4990  nfvres  5119  funimass4  5137  funconstss  5198  f1oresrab  5242  resfunexg  5295  f1eqcocnv  5344  isores1  5367  isoini  5370  isose  5373  isopolem  5374  isosolem  5376  eusvobj2  5410  acexmidlemcase  5419  oprabid  5449  offval  5630  resfunexgALT  5648  offval3  5672  1stvalg  5680  2ndvalg  5681  1stcof  5701  2ndcof  5702  cnvf1o  5757  tposf12  5794  smores3  5818  smoiso  5827  tfrlemibxssdm  5850  tfrlemi14d  5856  tfrexlem  5858  rdgss  5878  frecsuclemdm  5892  oei0  5942  nnsucsssuc  5974  swoord1  6034  swoord2  6035  iinerm  6077  eroveu  6096  addclnq  6220  mulclnq  6221  1qec  6233  prarloclemarch2  6262  enq0tr  6275  addclnq0  6292  mulclnq0  6293  nq0m0r  6297  prarloclemlo  6334  prarloc  6343  genpml  6358  genpmu  6359  addnqprl  6370  addnqpru  6371  prmuloc2  6397  1idpru  6416  ltexprlemm  6423  ltexprlemloc  6430  recexprlemm  6445  recexprlem1ssl  6454  addclsr  6491  mulclsr  6492  mulap0r  7202  nn1suc  7516  prime  7901  zindd  7920  bj-inex  8288  bj-sucexg  8303  bj-peano4  8339  setindis  8347  bdsetindis  8349  bj-inf2vnlem1  8350
  Copyright terms: Public domain W3C validator