Theorem ifan 3987

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

Assertion

Ref	Expression
ifan

Proof of Theorem ifan

Step	Hyp	Ref	Expression
1		iftrue 3947	. . 3
2		ibar 504	. . . 4
3	2	ifbid 3963	. . 3
4	1, 3	eqtr2d 2499	. 2
5		simpl 457	. . . . 5
6	5	con3i 135	. . . 4
7	6	iffalsed 3952	. . 3
8		iffalse 3950	. . 3
9	7, 8	eqtr4d 2501	. 2
10	4, 9	pm2.61i 164	1

Syntax hints:  -.wn 3  /\wa 369  =wceq 1395  ifcif 3941

This theorem is referenced by:  itg0  22186  iblre  22200  itgreval  22203  iblss  22211  iblss2  22212  itgle  22216  itgss  22218  itgeqa  22220  iblconst  22224  itgconst  22225  ibladdlem  22226  iblabslem  22234  iblabsr  22236  iblmulc2  22237  itgsplit  22242  itgcn  22249  mrsubrn  28873  itg2gt0cn  30070  ibladdnclem  30071  iblabsnclem  30078  iblmulc2nc  30080  bddiblnc  30085  iblsplit  31765

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-if 3942