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 1816	1 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑)

Syntax hints:   → wi 4  ∃*wmo 2563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-mo 2565

This theorem is referenced 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  5091  disjxsn  5093  axsepgfromrep  5243  fununmo  6564  funcnvsn  6567  nfunsn  6902  caovmo  7629  iunmapdisj  9976  brdom3  10482  brdom5  10483  brdom4  10484  nqerf  10885  shftfn  15083  2ndcdisj2  23497  plyexmo  26354  ajfuni  31008  funadj  32035  cnlnadjeui  32226  amosym1  36750  sinnpoly  47449  funressnvmo  47603