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	⊢ 𝐺 : 𝐴 ⟶ 𝐵
Assertion	elimf	⊢ if ( 𝐹 : 𝐴 ⟶ 𝐵 , 𝐹 , 𝐺 ) : 𝐴 ⟶ 𝐵

Proof

Step	Hyp	Ref	Expression
1		elimf.1	⊢ 𝐺 : 𝐴 ⟶ 𝐵
2		feq1	⊢ ( 𝐹 = if ( 𝐹 : 𝐴 ⟶ 𝐵 , 𝐹 , 𝐺 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ if ( 𝐹 : 𝐴 ⟶ 𝐵 , 𝐹 , 𝐺 ) : 𝐴 ⟶ 𝐵 ) )
3		feq1	⊢ ( 𝐺 = if ( 𝐹 : 𝐴 ⟶ 𝐵 , 𝐹 , 𝐺 ) → ( 𝐺 : 𝐴 ⟶ 𝐵 ↔ if ( 𝐹 : 𝐴 ⟶ 𝐵 , 𝐹 , 𝐺 ) : 𝐴 ⟶ 𝐵 ) )
4	2 3 1	elimhyp	⊢ if ( 𝐹 : 𝐴 ⟶ 𝐵 , 𝐹 , 𝐺 ) : 𝐴 ⟶ 𝐵