Theorem moimi 2546

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

Syntax hints:   → wi 4  ∃*wmo 2538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540

This theorem is referenced by:  moa1  2552  moan  2553  moor  2555  mooran1  2556  mooran2  2557  moaneu  2624  2moexv  2628  2euexv  2632  2exeuv  2633  2moex  2641  2euex  2642  2exeu  2647  sndisj  5092  disjxsn  5094  axsepgfromrep  5241  fununmo  6547  funcnvsn  6550  nfunsn  6881  caovmo  7605  iunmapdisj  9945  brdom3  10450  brdom5  10451  brdom4  10452  nqerf  10853  shftfn  15008  2ndcdisj2  23413  plyexmo  26289  ajfuni  30946  funadj  31973  cnlnadjeui  32164  amosym1  36639  sinnpoly  47245  funressnvmo  47399