Theorem ifan 3946

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 3908	. . 3 |- ( ph -> if ( ph , if ( ps , A , B ) , B ) = if ( ps , A , B ) )
2		ibar 504	. . . 4 |- ( ph -> ( ps <-> ( ph /\ ps ) ) )
3	2	ifbid 3922	. . 3 |- ( ph -> if ( ps , A , B ) = if ( ( ph /\ ps ) , A , B ) )
4	1, 3	eqtr2d 2496	. 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 3910	. . . 4 |- ( -. ( ph /\ ps ) -> if ( ( ph /\ ps ) , A , B ) = B )
8	6, 7	syl 16	. . 3 |- ( -. ph -> if ( ( ph /\ ps ) , A , B ) = B )
9		iffalse 3910	. . 3 |- ( -. ph -> if ( ph , if ( ps , A , B ) , B ) = B )
10	8, 9	eqtr4d 2498	. 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 1370   ifcif 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3903

This theorem is referenced by:  itg0  21393  iblre  21407  itgreval  21410  iblss  21418  iblss2  21419  itgle  21423  itgss  21425  itgeqa  21427  iblconst  21431  itgconst  21432  ibladdlem  21433  iblabslem  21441  iblabsr  21443  iblmulc2  21444  itgsplit  21449  itgcn  21456  itg2gt0cn  28615  ibladdnclem  28616  iblabsnclem  28623  iblmulc2nc  28625  bddiblnc  28630