Theorem ifan 3929

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 3889	. . 3 |- ( ph -> if ( ph , if ( ps , A , B ) , B ) = if ( ps , A , B ) )
2		ibar 507	. . . 4 |- ( ph -> ( ps <-> ( ph /\ ps ) ) )
3	2	ifbid 3905	. . 3 |- ( ph -> if ( ps , A , B ) = if ( ( ph /\ ps ) , A , B ) )
4	1, 3	eqtr2d 2488	. 2 |- ( ph -> if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B ) )
5		simpl 459	. . . . 5 |- ( ( ph /\ ps ) -> ph )
6	5	con3i 141	. . . 4 |- ( -. ph -> -. ( ph /\ ps ) )
7	6	iffalsed 3894	. . 3 |- ( -. ph -> if ( ( ph /\ ps ) , A , B ) = B )
8		iffalse 3892	. . 3 |- ( -. ph -> if ( ph , if ( ps , A , B ) , B ) = B )
9	7, 8	eqtr4d 2490	. 2 |- ( -. ph -> if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B ) )
10	4, 9	pm2.61i 168	1 |- if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B )

Syntax hints:   -. wn 3   /\ wa 371   = wceq 1446   ifcif 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3884

This theorem is referenced by:  itg0  22749  iblre  22763  itgreval  22766  iblss  22774  iblss2  22775  itgle  22779  itgss  22781  itgeqa  22783  iblconst  22787  itgconst  22788  ibladdlem  22789  iblabslem  22797  iblabsr  22799  iblmulc2  22800  itgsplit  22805  itgcn  22812  mrsubrn  30163  itg2gt0cn  32009  ibladdnclem  32010  iblabsnclem  32017  iblmulc2nc  32019  bddiblnc  32024  iblsplit  37853