Description: Theorem 5.7 of [Laboreo] 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 exnatded5.72 20787.
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 453 because we do not move this
into an ND hypothesis 
2  1  ... 

ND hypothesis assumption (new scope) 
simpr 449 
3  2  ... 

I_{L} 2 
orcd 383, the MPE equivalent of I_{L}, 1 
4  3  ... 

ND hypothesis assumption (new scope) 
simpr 449 
5  4  ... 

E_{L} 4 
simpld 447, the MPE equivalent of E_{L}, 3 
6  6  ... 

I_{R} 5 
olcd 384, the MPE equivalent of I_{R}, 4 
7  7  

E 1,3,6 
mpjaodan 764, 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 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.) 