ax-jca - Higher-Order Logic Explorer

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

Axiom ax-jca 17

Description: Join common antecedents. (Contributed by Mario Carneiro, 8-Oct-2014.)

**Hypotheses**
Ref	Expression
ax-jca.1	⊢ R⊧S
ax-jca.2	⊢ R⊧T

**Assertion**
Ref	Expression
ax-jca	⊢ R⊧(S, T)

**Detailed syntax breakdown of Axiom ax-jca**
Step	Hyp	Ref	Expression
1		tr	. 2 term R
2		ts	. . 3 term S
3		tt	. . 3 term T
4	2, 3	kct 10	. 2 term (S, T)
5	1, 4	wffMMJ2 11	1 wff R⊧(S, T)

Colors of variables: type var term

This axiom is referenced by: jca 18