Theorem moimi 2570

Description: The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006.)

Hypothesis

Ref	Expression
moimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
moimi	⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑)

Proof of Theorem moimi

Step	Hyp	Ref	Expression
1		moim 2569	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))
2		moimi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1830	1 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑)

This proof depends on syntax axioms:   → wi 4  ∃*wmo 2562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2564

This theorem is used by:  moa1  2576  moan  2577  moor  2579  mooran1  2580  mooran2  2581  moaneu  2648  2moexv  2652  2euexv  2656  2exeuv  2657  2moex  2665  2euex  2666  2exeu  2671  sndisj  5095  disjxsn  5097  axsepgfromrep  5249  fununmo  6580  funcnvsn  6583  nfunsn  6917  caovmo  7651  iunmapdisj  10026  brdom3  10531  brdom5  10532  brdom4  10533  nqerf  10939  shftfn  15146  2ndcdisj2  23683  plyexmo  26545  ajfuni  31340  funadj  32367  cnlnadjeui  32558  amosym1  37045  sinnpoly  47759  funressnvmo  47933