This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ex-natded9.20-2

Description: A more efficient proof of Theorem 9.20 of Clemente p. 45. Compare with ex-natded9.20 . (Contributed by David A. Wheeler, 19-Feb-2017) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	ex-natded9.20.1	\|- ( ph -> ( ps /\ ( ch \/ th ) ) )
	Assertion	ex-natded9.20-2	\|- ( ph -> ( ( ps /\ ch ) \/ ( ps /\ th ) ) )

Proof

Step	Hyp	Ref	Expression
1		ex-natded9.20.1	\|- ( ph -> ( ps /\ ( ch \/ th ) ) )
2	1	simpld	\|- ( ph -> ps )
3	2	anim1i	\|- ( ( ph /\ ch ) -> ( ps /\ ch ) )
4	3	orcd	\|- ( ( ph /\ ch ) -> ( ( ps /\ ch ) \/ ( ps /\ th ) ) )
5	2	anim1i	\|- ( ( ph /\ th ) -> ( ps /\ th ) )
6	5	olcd	\|- ( ( ph /\ th ) -> ( ( ps /\ ch ) \/ ( ps /\ th ) ) )
7	1	simprd	\|- ( ph -> ( ch \/ th ) )
8	4 6 7	mpjaodan	\|- ( ph -> ( ( ps /\ ch ) \/ ( ps /\ th ) ) )