Higher-Order Logic Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  jca		Unicode version

---

Theorem jca 18

Description: Syllogism inference.

Hypotheses

Ref	Expression
ax-jca.1
ax-jca.2

Assertion

Ref	Expression
jca

---

Proof of Theorem jca

Step	Hyp	Ref	Expression
1		ax-jca.1	. 2
2		ax-jca.2	. 2
3	1, 2	ax-jca 17	1

Colors of variables: type var term

Syntax hints:  kct 10   wffMMJ2 11

This theorem was proved from axioms:  ax-jca 17

This theorem is referenced by:  syl2anc  19  ct1  52  ct2  53  dfan2  144  ex  148

Copyright terms: Public domain

W3C validator