Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > cbv1h | GIF version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-May-2018.) |
Ref | Expression |
---|---|
cbv1h.1 | ⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) |
cbv1h.2 | ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) |
cbv1h.3 | ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) |
Ref | Expression |
---|---|
cbv1h | ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfa1 1474 | . 2 ⊢ Ⅎ𝑥∀𝑥∀𝑦𝜑 | |
2 | nfa2 1511 | . 2 ⊢ Ⅎ𝑦∀𝑥∀𝑦𝜑 | |
3 | sp 1441 | . . . . 5 ⊢ (∀𝑦𝜑 → 𝜑) | |
4 | 3 | sps 1470 | . . . 4 ⊢ (∀𝑥∀𝑦𝜑 → 𝜑) |
5 | cbv1h.1 | . . . 4 ⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) | |
6 | 4, 5 | syl 14 | . . 3 ⊢ (∀𝑥∀𝑦𝜑 → (𝜓 → ∀𝑦𝜓)) |
7 | 2, 6 | nfd 1456 | . 2 ⊢ (∀𝑥∀𝑦𝜑 → Ⅎ𝑦𝜓) |
8 | cbv1h.2 | . . . 4 ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) | |
9 | 4, 8 | syl 14 | . . 3 ⊢ (∀𝑥∀𝑦𝜑 → (𝜒 → ∀𝑥𝜒)) |
10 | 1, 9 | nfd 1456 | . 2 ⊢ (∀𝑥∀𝑦𝜑 → Ⅎ𝑥𝜒) |
11 | cbv1h.3 | . . 3 ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) | |
12 | 4, 11 | syl 14 | . 2 ⊢ (∀𝑥∀𝑦𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) |
13 | 1, 2, 7, 10, 12 | cbv1 1672 | 1 ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1282 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-4 1440 ax-i9 1463 ax-ial 1467 ax-i5r 1468 |
This theorem depends on definitions: df-bi 115 df-nf 1390 |
This theorem is referenced by: cbv2h 1674 |
Copyright terms: Public domain | W3C validator |