![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 19.33b2 | GIF version |
Description: The antecedent provides a condition implying the converse of 19.33 1370. Compare Theorem 19.33 of [Margaris] p. 90. This variation of 19.33bdc 1518 is intuitionistically valid without a decidability condition. (Contributed by Mario Carneiro, 2-Feb-2015.) |
Ref | Expression |
---|---|
19.33b2 | ⊢ ((¬ ∃xφ ∨ ¬ ∃xψ) → (∀x(φ ∨ ψ) ↔ (∀xφ ∨ ∀xψ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcom 646 | . . . . 5 ⊢ ((¬ ∃xφ ∨ ¬ ∃xψ) ↔ (¬ ∃xψ ∨ ¬ ∃xφ)) | |
2 | alnex 1385 | . . . . . 6 ⊢ (∀x ¬ ψ ↔ ¬ ∃xψ) | |
3 | alnex 1385 | . . . . . 6 ⊢ (∀x ¬ φ ↔ ¬ ∃xφ) | |
4 | 2, 3 | orbi12i 680 | . . . . 5 ⊢ ((∀x ¬ ψ ∨ ∀x ¬ φ) ↔ (¬ ∃xψ ∨ ¬ ∃xφ)) |
5 | 1, 4 | bitr4i 176 | . . . 4 ⊢ ((¬ ∃xφ ∨ ¬ ∃xψ) ↔ (∀x ¬ ψ ∨ ∀x ¬ φ)) |
6 | pm2.53 640 | . . . . . . 7 ⊢ ((ψ ∨ φ) → (¬ ψ → φ)) | |
7 | 6 | orcoms 648 | . . . . . 6 ⊢ ((φ ∨ ψ) → (¬ ψ → φ)) |
8 | 7 | al2imi 1344 | . . . . 5 ⊢ (∀x(φ ∨ ψ) → (∀x ¬ ψ → ∀xφ)) |
9 | pm2.53 640 | . . . . . 6 ⊢ ((φ ∨ ψ) → (¬ φ → ψ)) | |
10 | 9 | al2imi 1344 | . . . . 5 ⊢ (∀x(φ ∨ ψ) → (∀x ¬ φ → ∀xψ)) |
11 | 8, 10 | orim12d 699 | . . . 4 ⊢ (∀x(φ ∨ ψ) → ((∀x ¬ ψ ∨ ∀x ¬ φ) → (∀xφ ∨ ∀xψ))) |
12 | 5, 11 | syl5bi 141 | . . 3 ⊢ (∀x(φ ∨ ψ) → ((¬ ∃xφ ∨ ¬ ∃xψ) → (∀xφ ∨ ∀xψ))) |
13 | 12 | com12 27 | . 2 ⊢ ((¬ ∃xφ ∨ ¬ ∃xψ) → (∀x(φ ∨ ψ) → (∀xφ ∨ ∀xψ))) |
14 | 19.33 1370 | . 2 ⊢ ((∀xφ ∨ ∀xψ) → ∀x(φ ∨ ψ)) | |
15 | 13, 14 | impbid1 130 | 1 ⊢ ((¬ ∃xφ ∨ ¬ ∃xψ) → (∀x(φ ∨ ψ) ↔ (∀xφ ∨ ∀xψ))) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 98 ∨ wo 628 ∀wal 1240 ∃wex 1378 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 629 ax-5 1333 ax-gen 1335 ax-ie2 1380 |
This theorem depends on definitions: df-bi 110 df-tru 1245 df-fal 1248 |
This theorem is referenced by: 19.33bdc 1518 |
Copyright terms: Public domain | W3C validator |