Theorem ifan

Description: Rewrite a conjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Assertion	ifan	|- if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B )

Proof

Step	Hyp	Ref	Expression
1		iftrue	|- ( ph -> if ( ph , if ( ps , A , B ) , B ) = if ( ps , A , B ) )
2		ibar	|- ( ph -> ( ps <-> ( ph /\ ps ) ) )
3	2	ifbid	|- ( ph -> if ( ps , A , B ) = if ( ( ph /\ ps ) , A , B ) )
4	1 3	eqtr2d	|- ( ph -> if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B ) )
5		simpl	|- ( ( ph /\ ps ) -> ph )
6	5	con3i	|- ( -. ph -> -. ( ph /\ ps ) )
7	6	iffalsed	|- ( -. ph -> if ( ( ph /\ ps ) , A , B ) = B )
8		iffalse	|- ( -. ph -> if ( ph , if ( ps , A , B ) , B ) = B )
9	7 8	eqtr4d	|- ( -. ph -> if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B ) )
10	4 9	pm2.61i	|- if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B )