Description: Theorem 5.3 of [Laboreo] 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 20769.
A proof without context is shown in exnatded5.3i 20770.
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 453 to move it into the ND hypothesis 
2  5;6  

Given 
$e; adantr 453 to move it into the ND hypothesis 
3  1  ... 

ND hypothesis assumption 
simpr 449, to access the new assumption 
4  4  ... 

E 1,3 
mpd 16, the MPE equivalent of E, 1.3.
adantr 453 was used to transform its dependency
(we could also use imp 420 to get this directly from 1)

5  7  ... 

E 2,4 
mpd 16, the MPE equivalent of E, 4,6.
adantr 453 was used to transform its dependency 
6  8  ... 

I 4,5 
jca 520, the MPE equivalent of I, 4,7 
7  9  

I 3,6 
ex 425, 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.
(Proof modification is discouraged.)
(Contributed by Mario Carneiro, 9Feb2017.) 