Description: Theorem 5.2 of [Clemente] p. 15, translated line by line using the
interpretation of natural deduction in Metamath.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows:
| # | MPE# | ND Expression |
MPE Translation | ND Rationale |
MPE Rationale |
|---|
| 1 | 5 | ((𝜓 ∧ 𝜒) → 𝜃) |
(𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Given |
$e. |
| 2 | 2 | (𝜒 → 𝜓) |
(𝜑 → (𝜒 → 𝜓)) |
Given |
$e. |
| 3 | 1 | 𝜒 |
(𝜑 → 𝜒) |
Given |
$e. |
| 4 | 3 | 𝜓 |
(𝜑 → 𝜓) |
→E 2,3 |
mpd 15, the MPE equivalent of →E, 1,2 |
| 5 | 4 | (𝜓 ∧ 𝜒) |
(𝜑 → (𝜓 ∧ 𝜒)) |
∧I 4,3 |
jca 512, the MPE equivalent of ∧I, 3,1 |
| 6 | 6 | 𝜃 |
(𝜑 → 𝜃) |
→E 1,5 |
mpd 15, the MPE equivalent of →E, 4,5 |
The original used Latin letters for predicates;
we have replaced them with
Greek letters to follow Metamath naming conventions and so that
it is easier to follow the Metamath translation.
The Metamath line-for-line translation of this
natural deduction approach precedes every line with an antecedent
including 𝜑 and uses the Metamath equivalents
of the natural deduction rules.
Below is the final Metamath proof (which reorders some steps).
A much more efficient proof, using more of Metamath and MPE's
capabilities, is shown in ex-natded5.2-2 28769.
A proof without context is shown in ex-natded5.2i 28770.
(Contributed by Mario Carneiro, 9-Feb-2017.)
(Proof modification is discouraged.) (New usage is
discouraged.) |
