| Description: Theorem 5.3 of [Clemente] p. 16, translated line by line using an
interpretation of natural deduction in Metamath.
A much more efficient proof, using more of Metamath and MPE's
capabilities, is shown in ex-natded5.3-2 28673.
A proof without context is shown in ex-natded5.3i 28674.
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 | 2;3 | (𝜓 → 𝜒) |
(𝜑 → (𝜓 → 𝜒)) |
Given |
$e; adantr 480 to move it into the ND hypothesis |
| 2 | 5;6 | (𝜒 → 𝜃) |
(𝜑 → (𝜒 → 𝜃)) |
Given |
$e; adantr 480 to move it into the ND hypothesis |
| 3 | 1 | ...| 𝜓 |
((𝜑 ∧ 𝜓) → 𝜓) |
ND hypothesis assumption |
simpr 484, to access the new assumption |
| 4 | 4 | ... 𝜒 |
((𝜑 ∧ 𝜓) → 𝜒) |
→E 1,3 |
mpd 15, the MPE equivalent of →E, 1.3.
adantr 480 was used to transform its dependency
(we could also use imp 406 to get this directly from 1)
|
| 5 | 7 | ... 𝜃 |
((𝜑 ∧ 𝜓) → 𝜃) |
→E 2,4 |
mpd 15, the MPE equivalent of →E, 4,6.
adantr 480 was used to transform its dependency |
| 6 | 8 | ... (𝜒 ∧ 𝜃) |
((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃)) |
∧I 4,5 |
jca 511, the MPE equivalent of ∧I, 4,7 |
| 7 | 9 | (𝜓 → (𝜒 ∧ 𝜃)) |
(𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) |
→I 3,6 |
ex 412, the MPE equivalent of →I, 8 |
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.
(Contributed by Mario Carneiro, 9-Feb-2017.)
(Proof modification is discouraged.) (New usage is
discouraged.) |
