Theorem csbif 3991

Description: Distribute proper substitution through the conditional operator. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 19-Aug-2018.)

Assertion

Ref	Expression
csbif

Proof of Theorem csbif

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		csbeq1 3437	. . . 4
2		dfsbcq2 3330	. . . . 5
3		csbeq1 3437	. . . . 5
4		csbeq1 3437	. . . . 5
5	2, 3, 4	ifbieq12d 3968	. . . 4
6	1, 5	eqeq12d 2479	. . 3
7		vex 3112	. . . 4
8		nfs1v 2181	. . . . 5
9		nfcsb1v 3450	. . . . 5
10		nfcsb1v 3450	. . . . 5
11	8, 9, 10	nfif 3970	. . . 4
12		sbequ12 1992	. . . . 5
13		csbeq1a 3443	. . . . 5
14		csbeq1a 3443	. . . . 5
15	12, 13, 14	ifbieq12d 3968	. . . 4
16	7, 11, 15	csbief 3459	. . 3
17	6, 16	vtoclg 3167	. 2
18		csbprc 3821	. . 3
19		csbprc 3821	. . . . 5
20		csbprc 3821	. . . . 5
21	19, 20	ifeq12d 3961	. . . 4
22		ifid 3978	. . . 4
23	21, 22	syl6req 2515	. . 3
24	18, 23	eqtrd 2498	. 2
25	17, 24	pm2.61i 164	1

Syntax hints:  -.wn 3  =wceq 1395  [wsb 1739  e.wcel 1818  cvv 3109  [.wsbc 3327  [_csb 3434  c0 3784  ifcif 3941

This theorem is referenced by:  fvmptnn04if  19350  cdlemk40  36643

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-3an 975  df-tru 1398  df-fal 1401  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942