Theorem ifan 3985

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

Assertion

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

Proof of Theorem ifan

Step	Hyp	Ref	Expression
1		iftrue 3945	. . 3 |- ( ph -> if ( ph , if ( ps , A , B ) , B ) = if ( ps , A , B ) )
2		ibar 504	. . . 4 |- ( ph -> ( ps <-> ( ph /\ ps ) ) )
3	2	ifbid 3961	. . 3 |- ( ph -> if ( ps , A , B ) = if ( ( ph /\ ps ) , A , B ) )
4	1, 3	eqtr2d 2509	. 2 |- ( ph -> if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B ) )
5		simpl 457	. . . . 5 |- ( ( ph /\ ps ) -> ph )
6	5	con3i 135	. . . 4 |- ( -. ph -> -. ( ph /\ ps ) )
7		iffalse 3948	. . . 4 |- ( -. ( ph /\ ps ) -> if ( ( ph /\ ps ) , A , B ) = B )
8	6, 7	syl 16	. . 3 |- ( -. ph -> if ( ( ph /\ ps ) , A , B ) = B )
9		iffalse 3948	. . 3 |- ( -. ph -> if ( ph , if ( ps , A , B ) , B ) = B )
10	8, 9	eqtr4d 2511	. 2 |- ( -. ph -> if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B ) )
11	4, 10	pm2.61i 164	1 |- if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B )

Syntax hints:   -. wn 3   /\ wa 369   = wceq 1379   ifcif 3939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3940

This theorem is referenced by:  itg0  22013  iblre  22027  itgreval  22030  iblss  22038  iblss2  22039  itgle  22043  itgss  22045  itgeqa  22047  iblconst  22051  itgconst  22052  ibladdlem  22053  iblabslem  22061  iblabsr  22063  iblmulc2  22064  itgsplit  22069  itgcn  22076  mrsubrn  28624  itg2gt0cn  29923  ibladdnclem  29924  iblabsnclem  29931  iblmulc2nc  29933  bddiblnc  29938  iblsplit  31511