Theorem moimi 2576

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

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

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 2570

This theorem is used by:  moa1  2582  moan  2583  moor  2585  mooran1  2586  mooran2  2587  moaneu  2654  2moexv  2658  2euexv  2662  2exeuv  2663  2moex  2671  2euex  2672  2exeu  2677  sndisj  5106  disjxsn  5108  axsepgfromrep  5260  fununmo  6590  funcnvsn  6593  nfunsn  6927  caovmo  7660  iunmapdisj  10026  brdom3  10530  brdom5  10531  brdom4  10532  nqerf  10933  shftfn  15136  2ndcdisj2  23651  plyexmo  26511  ajfuni  31248  funadj  32275  cnlnadjeui  32466  amosym1  36978  sinnpoly  47669  funressnvmo  47823