Theorem elimif

Description: Elimination of a conditional operator contained in a wff ps . (Contributed by NM, 15-Feb-2005) (Proof shortened by NM, 25-Apr-2019)

	Ref	Expression
Hypotheses	elimif.1	|- ( if ( ph , A , B ) = A -> ( ps <-> ch ) )
	elimif.2	|- ( if ( ph , A , B ) = B -> ( ps <-> th ) )
Assertion	elimif	|- ( ps <-> ( ( ph /\ ch ) \/ ( -. ph /\ th ) ) )

Proof

Step	Hyp	Ref	Expression
1		elimif.1	|- ( if ( ph , A , B ) = A -> ( ps <-> ch ) )
2		elimif.2	|- ( if ( ph , A , B ) = B -> ( ps <-> th ) )
3		iftrue	|- ( ph -> if ( ph , A , B ) = A )
4	3 1	syl	|- ( ph -> ( ps <-> ch ) )
5		iffalse	|- ( -. ph -> if ( ph , A , B ) = B )
6	5 2	syl	|- ( -. ph -> ( ps <-> th ) )
7	4 6	cases	|- ( ps <-> ( ( ph /\ ch ) \/ ( -. ph /\ th ) ) )