Theorem a1bi

Description: Inference introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993) (Proof shortened by Wolf Lammen, 11-Nov-2012)

	Ref	Expression
Hypothesis	a1bi.1	|- ph
Assertion	a1bi	|- ( ps <-> ( ph -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		a1bi.1	|- ph
2		biimt	|- ( ph -> ( ps <-> ( ph -> ps ) ) )
3	1 2	ax-mp	|- ( ps <-> ( ph -> ps ) )