Theorem elimf

Description: Eliminate a mapping hypothesis for the weak deduction theorem dedth , when a special case G : A --> B is provable, in order to convert F : A --> B from a hypothesis to an antecedent. (Contributed by NM, 24-Aug-2006)

	Ref	Expression
Hypothesis	elimf.1	$$⊢G:A⟶B$$
Assertion	elimf	$$⊢if\left(F:A⟶B,F,G\right):A⟶B$$

Proof

Step	Hyp	Ref	Expression
1		elimf.1	$$⊢G:A⟶B$$
2		feq1	$$⊢F=if\left(F:A⟶B,F,G\right)\to \left(F:A⟶B\leftrightarrow if\left(F:A⟶B,F,G\right):A⟶B\right)$$
3		feq1	$$⊢G=if\left(F:A⟶B,F,G\right)\to \left(G:A⟶B\leftrightarrow if\left(F:A⟶B,F,G\right):A⟶B\right)$$
4	2 3 1	elimhyp	$$⊢if\left(F:A⟶B,F,G\right):A⟶B$$