![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfif | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for a conditional operator. (Contributed by NM, 16-Feb-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
nfif.1 | ⊢ Ⅎ𝑥𝜑 |
nfif.2 | ⊢ Ⅎ𝑥𝐴 |
nfif.3 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfif | ⊢ Ⅎ𝑥if(𝜑, 𝐴, 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfif.1 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
3 | nfif.2 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
4 | 3 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
5 | nfif.3 | . . . 4 ⊢ Ⅎ𝑥𝐵 | |
6 | 5 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐵) |
7 | 2, 4, 6 | nfifd 4514 | . 2 ⊢ (⊤ → Ⅎ𝑥if(𝜑, 𝐴, 𝐵)) |
8 | 7 | mptru 1548 | 1 ⊢ Ⅎ𝑥if(𝜑, 𝐴, 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1542 Ⅎwnf 1785 Ⅎwnfc 2886 ifcif 4485 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2888 df-if 4486 |
This theorem is referenced by: csbif 4542 nfop 4845 nfrdg 8357 boxcutc 8876 nfoi 9447 nfsum1 15571 nfsum 15572 nfsumOLD 15573 summolem2a 15597 zsum 15600 sumss 15606 sumss2 15608 fsumcvg2 15609 nfcprod 15791 cbvprod 15795 prodmolem2a 15814 zprod 15817 fprod 15821 fprodntriv 15822 prodss 15827 pcmpt 16761 pcmptdvds 16763 gsummpt1n0 19738 madugsum 21988 mbfpos 25011 mbfposb 25013 i1fposd 25068 isibl2 25127 nfitg 25135 cbvitg 25136 itgss3 25175 itgcn 25205 limcmpt 25243 rlimcnp2 26312 nosupbnd2 27060 noinfbnd2 27075 chirred 31235 cdleme31sn 38832 cdleme32d 38896 cdleme32f 38898 refsum2cn 43223 ssfiunibd 43517 uzub 43640 limsupubuz 43924 icccncfext 44098 fourierdlem86 44403 vonicc 44896 nfafv 45338 nfafv2 45420 |
Copyright terms: Public domain | W3C validator |