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 ( F : A --> B , F , G ) : A --> B

Proof

Step	Hyp	Ref	Expression
1		elimf.1	|- G : A --> B
2		feq1	|- ( F = if ( F : A --> B , F , G ) -> ( F : A --> B <-> if ( F : A --> B , F , G ) : A --> B ) )
3		feq1	|- ( G = if ( F : A --> B , F , G ) -> ( G : A --> B <-> if ( F : A --> B , F , G ) : A --> B ) )
4	2 3 1	elimhyp	|- if ( F : A --> B , F , G ) : A --> B