Theorem ex-natded5.7 27268

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 27269. 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	( ps \/ ( ch /\ th ) )	( ph -> ( ps \/ ( ch /\ th ) ) )	Given	$e. No need for adantr 481 because we do not move this into an ND hypothesis
2	1	...| ps	( ( ph /\ ps ) -> ps )	ND hypothesis assumption (new scope)	simpr 477
3	2	... ( ps \/ ch )	( ( ph /\ ps ) -> ( ps \/ ch ) )	\/IL 2	orcd 407, the MPE equivalent of \/IL, 1
4	3	...| ( ch /\ th )	( ( ph /\ ( ch /\ th ) ) -> ( ch /\ th ) )	ND hypothesis assumption (new scope)	simpr 477
5	4	... ch	( ( ph /\ ( ch /\ th ) ) -> ch )	/\EL 4	simpld 475, the MPE equivalent of /\EL, 3
6	6	... ( ps \/ ch )	( ( ph /\ ( ch /\ th ) ) -> ( ps \/ ch ) )	\/IR 5	olcd 408, the MPE equivalent of \/IR, 4
7	7	( ps \/ ch )	( ph -> ( ps \/ ch ) )	\/E 1,3,6	mpjaodan 827, 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 ph 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.)

Hypothesis

Ref	Expression
ex-natded5.7.1	|- ( ph -> ( ps \/ ( ch /\ th ) ) )

Assertion

Ref	Expression
ex-natded5.7	|- ( ph -> ( ps \/ ch ) )

Proof of Theorem ex-natded5.7

Step	Hyp	Ref	Expression
1		simpr 477	. . 3 |- ( ( ph /\ ps ) -> ps )
2	1	orcd 407	. 2 |- ( ( ph /\ ps ) -> ( ps \/ ch ) )
3		simpr 477	. . . 4 |- ( ( ph /\ ( ch /\ th ) ) -> ( ch /\ th ) )
4	3	simpld 475	. . 3 |- ( ( ph /\ ( ch /\ th ) ) -> ch )
5	4	olcd 408	. 2 |- ( ( ph /\ ( ch /\ th ) ) -> ( ps \/ ch ) )
6		ex-natded5.7.1	. 2 |- ( ph -> ( ps \/ ( ch /\ th ) ) )
7	2, 5, 6	mpjaodan 827	1 |- ( ph -> ( ps \/ ch ) )

Syntax hints:   -> wi 4   \/ wo 383   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386

This theorem is referenced by: (None)