Metamath Proof Explorer


Theorem moimdv

Description: The at-most-one quantifier reverses implication, deduction form. (Contributed by Thierry Arnoux, 25-Feb-2017)

Ref Expression
Hypothesis moimdv.1 φψχ
Assertion moimdv φ*xχ*xψ

Proof

Step Hyp Ref Expression
1 moimdv.1 φψχ
2 1 alrimiv φxψχ
3 moim xψχ*xχ*xψ
4 2 3 syl φ*xχ*xψ