Theorem ifboth

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

	Ref	Expression
Hypotheses	ifboth.1	|- ( A = if ( ph , A , B ) -> ( ps <-> th ) )
	ifboth.2	|- ( B = if ( ph , A , B ) -> ( ch <-> th ) )
Assertion	ifboth	|- ( ( ps /\ ch ) -> 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		simpll	|- ( ( ( ps /\ ch ) /\ ph ) -> ps )
4		simplr	|- ( ( ( ps /\ ch ) /\ -. ph ) -> ch )
5	1 2 3 4	ifbothda	|- ( ( ps /\ ch ) -> th )