Theorem ifbothda

Description: A wff th containing a conditional operator is true when both of its cases are true. (Contributed by NM, 15-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ifboth.1	|- ( A = if ( ph , A , B ) -> ( ps <-> th ) )
2		ifboth.2	|- ( B = if ( ph , A , B ) -> ( ch <-> th ) )
3		ifbothda.3	|- ( ( et /\ ph ) -> ps )
4		ifbothda.4	|- ( ( et /\ -. ph ) -> ch )
5		iftrue	|- ( ph -> if ( ph , A , B ) = A )
6	5	eqcomd	|- ( ph -> A = if ( ph , A , B ) )
7	6 1	syl	|- ( ph -> ( ps <-> th ) )
8	7	adantl	|- ( ( et /\ ph ) -> ( ps <-> th ) )
9	3 8	mpbid	|- ( ( et /\ ph ) -> th )
10		iffalse	|- ( -. ph -> if ( ph , A , B ) = B )
11	10	eqcomd	|- ( -. ph -> B = if ( ph , A , B ) )
12	11 2	syl	|- ( -. ph -> ( ch <-> th ) )
13	12	adantl	|- ( ( et /\ -. ph ) -> ( ch <-> th ) )
14	4 13	mpbid	|- ( ( et /\ -. ph ) -> th )
15	9 14	pm2.61dan	|- ( et -> th )