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 exnatded5.32 27601.
A proof without context is shown in exnatded5.3i 27602.
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 466 to move it into the ND hypothesis 
2  5;6  (𝜒 → 𝜃) 
(𝜑 → (𝜒 → 𝜃)) 
Given 
$e; adantr 466 to move it into the ND hypothesis 
3  1  ... 𝜓 
((𝜑 ∧ 𝜓) → 𝜓) 
ND hypothesis assumption 
simpr 471, to access the new assumption 
4  4  ... 𝜒 
((𝜑 ∧ 𝜓) → 𝜒) 
→E 1,3 
mpd 15, the MPE equivalent of →E, 1.3.
adantr 466 was used to transform its dependency
(we could also use imp 393 to get this directly from 1)

5  7  ... 𝜃 
((𝜑 ∧ 𝜓) → 𝜃) 
→E 2,4 
mpd 15, the MPE equivalent of →E, 4,6.
adantr 466 was used to transform its dependency 
6  8  ... (𝜒 ∧ 𝜃) 
((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃)) 
∧I 4,5 
jca 495, the MPE equivalent of ∧I, 4,7 
7  9  (𝜓 → (𝜒 ∧ 𝜃)) 
(𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) 
→I 3,6 
ex 397, 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 lineforline 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, 9Feb2017.)
(Proof modification is discouraged.) (New usage is
discouraged.) 