Theorem nfif 3563

Description: Bound-variable hypothesis builder for a conditional operator. (Contributed by NM, 16-Feb-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Hypotheses

Ref	Expression
nfif.1	|- F/ x ph
nfif.2	|- F/_ x A
nfif.3	|- F/_ x B

Assertion

Ref	Expression
nfif	|- F/_ x if ( ph , A , B )

Proof of Theorem nfif

Step	Hyp	Ref	Expression
1		nfif.1	. . . 4 |- F/ x ph
2	1	a1i 9	. . 3 |- ( T. -> F/ x ph )
3		nfif.2	. . . 4 |- F/_ x A
4	3	a1i 9	. . 3 |- ( T. -> F/_ x A )
5		nfif.3	. . . 4 |- F/_ x B
6	5	a1i 9	. . 3 |- ( T. -> F/_ x B )
7	2, 4, 6	nfifd 3562	. 2 |- ( T. -> F/_ x if ( ph , A , B ) )
8	7	mptru 1362	1 |- F/_ x if ( ph , A , B )

Syntax hints:   T. wtru 1354   F/wnf 1460   F/_wnfc 2306   ifcif 3535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-if 3536

This theorem is referenced by:  nfsum1  11364  nfsum  11365  sumrbdclem  11385  summodclem2a  11389  zsumdc  11392  fsum3  11395  isumss  11399  isumss2  11401  fsum3cvg2  11402  nfcprod1  11562  nfcprod  11563  cbvprod  11566  prodrbdclem  11579  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  fprodntrivap  11592  prodssdc  11597  pcmpt  12341  pcmptdvds  12343