HomeRelated theorems
GIF version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems GIF version |
| Description: Peirce's axiom. This odd-looking theorem is the "difference" between an intuitionistic system of propositional calculus and a classical system and is not accepted by intuitionists. When Peirce's axiom is added to an intuitionistic system, the system becomes equivalent to our classical system ax-1 4 through ax-3 6. A curious fact about this theorem is that it requires ax-3 6 for its proof even though the result has no negation connectives in it. |
| Ref | Expression |
|---|---|
| peirce | ⊢ (((φ → ψ) → φ) → φ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm2.21 76 | . . 3 ⊢ (¬ φ → (φ → ψ)) | |
| 2 | 1 | imim1i 16 | . 2 ⊢ (((φ → ψ) → φ) → (¬ φ → φ)) |
| 3 | pm2.18 81 | . 2 ⊢ ((¬ φ → φ) → φ) | |
| 4 | 2, 3 | syl 10 | 1 ⊢ (((φ → ψ) → φ) → φ) |
| Colors of variables: wff set class |
| Syntax hints: ¬ wn 2 → wi 3 |
| This theorem is referenced by: looinv 83 exmoeu 1406 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 |