Theorem idi 1290

Description: Deduction form of id 73. Derived automatically from idiVD 16688. (Contributed by Alan Sare, 31-Dec-2011.)

Hypothesis

Ref	Expression
idi.1	|- ph

Assertion

Ref	Expression
idi	|- ph

Proof of Theorem idi

Step	Hyp	Ref	Expression
1		idi.1	. 2 |- ph
2		id 73	. 2 |- (ph -> ph)
3	1, 2	ax-mp 7	1 |- ph

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain