| Description: Theorem 5.7 of [Clemente] p. 19, translated line by line using the
interpretation of natural deduction in Metamath.
A much more efficient proof, using more of Metamath and MPE's
capabilities, is shown in ex-natded5.7-2 28776.
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 | 6 |
(𝜓 ∨ (𝜒 ∧ 𝜃)) |
(𝜑 → (𝜓 ∨ (𝜒 ∧ 𝜃))) |
Given |
$e. No need for adantr 481 because we do not move this
into an ND hypothesis |
| 2 | 1 | ...| 𝜓 |
((𝜑 ∧ 𝜓) → 𝜓) |
ND hypothesis assumption (new scope) |
simpr 485 |
| 3 | 2 | ... (𝜓 ∨ 𝜒) |
((𝜑 ∧ 𝜓) → (𝜓 ∨ 𝜒)) |
∨IL 2 |
orcd 870, the MPE equivalent of ∨IL, 1 |
| 4 | 3 | ...| (𝜒 ∧ 𝜃) |
((𝜑 ∧ (𝜒 ∧ 𝜃)) → (𝜒 ∧ 𝜃)) |
ND hypothesis assumption (new scope) |
simpr 485 |
| 5 | 4 | ... 𝜒 |
((𝜑 ∧ (𝜒 ∧ 𝜃)) → 𝜒) |
∧EL 4 |
simpld 495, the MPE equivalent of ∧EL, 3 |
| 6 | 6 | ... (𝜓 ∨ 𝜒) |
((𝜑 ∧ (𝜒 ∧ 𝜃)) → (𝜓 ∨ 𝜒)) |
∨IR 5 |
olcd 871, the MPE equivalent of ∨IR, 4 |
| 7 | 7 | (𝜓 ∨ 𝜒) |
(𝜑 → (𝜓 ∨ 𝜒)) |
∨E 1,3,6 |
mpjaodan 956, the MPE equivalent of ∨E, 2,5,6 |
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.) |
