| 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 4555 | . 2 ⊢ (⊤ → Ⅎ𝑥if(𝜑, 𝐴, 𝐵)) |
| 8 | 7 | mptru 1547 | 1 ⊢ Ⅎ𝑥if(𝜑, 𝐴, 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ⊤wtru 1541 Ⅎwnf 1783 Ⅎwnfc 2890 ifcif 4525 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-if 4526 |
| This theorem is referenced by: csbif 4583 nfop 4889 nfrdg 8454 boxcutc 8981 nfoi 9554 nfsum1 15726 nfsum 15727 summolem2a 15751 zsum 15754 sumss 15760 sumss2 15762 fsumcvg2 15763 nfcprod 15945 cbvprod 15949 prodmolem2a 15970 zprod 15973 fprod 15977 fprodntriv 15978 prodss 15983 pcmpt 16930 pcmptdvds 16932 gsummpt1n0 19983 madugsum 22649 mbfpos 25686 mbfposb 25688 i1fposd 25742 isibl2 25801 nfitg 25810 cbvitg 25811 itgss3 25850 itgcn 25880 limcmpt 25918 rlimcnp2 27009 nosupbnd2 27761 noinfbnd2 27776 chirred 32414 cdleme31sn 40382 cdleme32d 40446 cdleme32f 40448 refsum2cn 45043 ssfiunibd 45321 uzub 45442 limsupubuz 45728 icccncfext 45902 fourierdlem86 46207 vonicc 46700 nfafv 47148 nfafv2 47230 |
| Copyright terms: Public domain | W3C validator |