Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nic-mp | Structured version Visualization version GIF version |
Description: Derive Nicod's rule of modus ponens using 'nand', from the standard one. Although the major and minor premise together also imply 𝜒, this form is necessary for useful derivations from nic-ax 1589. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to an axiom ($a statement). (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nic-jmin | ⊢ 𝜑 |
nic-jmaj | ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓)) |
Ref | Expression |
---|---|
nic-mp | ⊢ 𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nic-jmin | . 2 ⊢ 𝜑 | |
2 | nic-jmaj | . . . 4 ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓)) | |
3 | nannan 1443 | . . . 4 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ↔ (𝜑 → (𝜒 ∧ 𝜓))) | |
4 | 2, 3 | mpbi 219 | . . 3 ⊢ (𝜑 → (𝜒 ∧ 𝜓)) |
5 | 4 | simprd 478 | . 2 ⊢ (𝜑 → 𝜓) |
6 | 1, 5 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ⊼ wnan 1439 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 df-an 385 df-nan 1440 |
This theorem is referenced by: nic-imp 1591 nic-idlem2 1593 nic-id 1594 nic-swap 1595 nic-isw1 1596 nic-isw2 1597 nic-iimp1 1598 nic-idel 1600 nic-ich 1601 nic-stdmp 1606 nic-luk1 1607 nic-luk2 1608 nic-luk3 1609 lukshefth1 1611 lukshefth2 1612 renicax 1613 |
Copyright terms: Public domain | W3C validator |