![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfif | 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 9 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
3 | nfif.2 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
4 | 3 | a1i 9 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
5 | nfif.3 | . . . 4 ⊢ Ⅎ𝑥𝐵 | |
6 | 5 | a1i 9 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐵) |
7 | 2, 4, 6 | nfifd 3576 | . 2 ⊢ (⊤ → Ⅎ𝑥if(𝜑, 𝐴, 𝐵)) |
8 | 7 | mptru 1373 | 1 ⊢ Ⅎ𝑥if(𝜑, 𝐴, 𝐵) |
Colors of variables: wff set class |
Syntax hints: ⊤wtru 1365 Ⅎwnf 1471 Ⅎwnfc 2319 ifcif 3549 |
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 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-if 3550 |
This theorem is referenced by: nfsum1 11396 nfsum 11397 sumrbdclem 11417 summodclem2a 11421 zsumdc 11424 fsum3 11427 isumss 11431 isumss2 11433 fsum3cvg2 11434 nfcprod1 11594 nfcprod 11595 cbvprod 11598 prodrbdclem 11611 prodmodclem2a 11616 zproddc 11619 fprodseq 11623 fprodntrivap 11624 prodssdc 11629 pcmpt 12375 pcmptdvds 12377 |
Copyright terms: Public domain | W3C validator |