Theorem moimi 2545

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

Syntax hints:   → wi 4  ∃*wmo 2537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2539

This theorem is referenced by:  moa1  2551  moan  2552  moor  2554  mooran1  2555  mooran2  2556  moaneu  2623  2moexv  2627  2euexv  2631  2exeuv  2632  2moex  2640  2euex  2641  2exeu  2646  sndisj  5090  disjxsn  5092  axsepgfromrep  5239  fununmo  6539  funcnvsn  6542  nfunsn  6873  caovmo  7595  iunmapdisj  9933  brdom3  10438  brdom5  10439  brdom4  10440  nqerf  10841  shftfn  14996  2ndcdisj2  23401  plyexmo  26277  ajfuni  30934  funadj  31961  cnlnadjeui  32152  amosym1  36620  sinnpoly  47133  funressnvmo  47287