Theorem moimi 2571

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 2570	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))
2		moimi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1830	1 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑)

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

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 2565

This theorem is used by:  moa1  2577  moan  2578  moor  2580  mooran1  2581  mooran2  2582  moaneu  2649  2moexv  2653  2euexv  2657  2exeuv  2658  2moex  2666  2euex  2667  2exeu  2672  sndisj  5095  disjxsn  5097  axsepgfromrep  5247  fununmo  6579  funcnvsn  6582  nfunsn  6916  caovmo  7650  iunmapdisj  10083  brdom3  10588  brdom5  10589  brdom4  10590  nqerf  10996  shftfn  15206  2ndcdisj2  23756  plyexmo  26618  ajfuni  31443  funadj  32470  cnlnadjeui  32661  amosym1  37184  sinnpoly  47885  funressnvmo  48059