Metamath Proof Explorer

Theorem moimiOLD

Description: Obsolete version of moimi as of 9-May-2023. The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis moimiOLD.1 φ ψ
Assertion moimiOLD * x ψ * x φ


Step Hyp Ref Expression
1 moimiOLD.1 φ ψ
2 moim x φ ψ * x ψ * x φ
3 2 1 mpg * x ψ * x φ