Theorem moimi 2573

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

Syntax hints:   → wi 4  ∃*wmo 2565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-mo 2567

This theorem is referenced by:  moa1  2579  moan  2580  moor  2582  mooran1  2583  mooran2  2584  moaneu  2651  2moexv  2655  2euexv  2659  2exeuv  2660  2moex  2668  2euex  2669  2exeu  2674  sndisj  5102  disjxsn  5104  axsepgfromrep  5256  fununmo  6585  funcnvsn  6588  nfunsn  6922  caovmo  7649  iunmapdisj  10008  brdom3  10513  brdom5  10514  brdom4  10515  nqerf  10916  shftfn  15112  2ndcdisj2  23595  plyexmo  26455  ajfuni  31189  funadj  32216  cnlnadjeui  32407  amosym1  36915  sinnpoly  47605  funressnvmo  47759