Theorem mpnanrd

Description: Eliminate the right side of a negated conjunction in an implication. (Contributed by ML, 17-Oct-2020)

	Ref	Expression
Hypotheses	mpnanrd.1	|- ( ph -> ps )
	mpnanrd.2	|- ( ph -> -. ( ps /\ ch ) )
Assertion	mpnanrd	|- ( ph -> -. ch )

Proof

Step	Hyp	Ref	Expression
1		mpnanrd.1	|- ( ph -> ps )
2		mpnanrd.2	|- ( ph -> -. ( ps /\ ch ) )
3		imnan	|- ( ( ps -> -. ch ) <-> -. ( ps /\ ch ) )
4	2 3	sylibr	|- ( ph -> ( ps -> -. ch ) )
5	1 4	mpd	|- ( ph -> -. ch )