Theorem ax12i 1738

Description: Inference that has ax-12 1854 (without A.) as its conclusion. Uses only Tarski's FOL axiom schemes. The hypotheses may be eliminable without one or more of these axioms in special cases. Proof similar to Lemma 16 of [Tarski] p. 70. (Contributed by NM, 20-May-2008.)

Hypotheses

Ref	Expression
ax12i.1
ax12i.2

Assertion

Ref	Expression
ax12i

Proof of Theorem ax12i

Step	Hyp	Ref	Expression
1		ax12i.1	. 2
2		ax12i.2	. . 3
3	1	biimprcd 225	. . 3
4	2, 3	alrimih 1642	. 2
5	1, 4	syl6bi 228	1

Syntax hints:  ->wi 4  <->wb 184  A.wal 1393

This theorem is referenced by:  ax12wlem  1828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631

This theorem depends on definitions:  df-bi 185