Theorem keephyp

Description: Transform a hypothesis ps that we want to keep (but contains the same class variable A used in the eliminated hypothesis) for use with the weak deduction theorem. (Contributed by NM, 15-May-1999)

	Ref	Expression
Hypotheses	keephyp.1	|- ( A = if ( ph , A , B ) -> ( ps <-> th ) )
	keephyp.2	|- ( B = if ( ph , A , B ) -> ( ch <-> th ) )
	keephyp.3	|- ps
	keephyp.4	|- ch
Assertion	keephyp	|- th

Proof

Step	Hyp	Ref	Expression
1		keephyp.1	|- ( A = if ( ph , A , B ) -> ( ps <-> th ) )
2		keephyp.2	|- ( B = if ( ph , A , B ) -> ( ch <-> th ) )
3		keephyp.3	|- ps
4		keephyp.4	|- ch
5	1 2	ifboth	|- ( ( ps /\ ch ) -> th )
6	3 4 5	mp2an	|- th