Theorem moimi 2575

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

Syntax hints:   → wi 4  ∃*wmo 2567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-mo 2569

This theorem is referenced by:  moa1  2581  moan  2582  moor  2584  mooran1  2585  mooran2  2586  moaneu  2653  2moexv  2657  2euexv  2661  2exeuv  2662  2moex  2670  2euex  2671  2exeu  2676  sndisj  5097  disjxsn  5099  axsepgfromrep  5249  fununmo  6572  funcnvsn  6575  nfunsn  6910  caovmo  7637  iunmapdisj  9995  brdom3  10500  brdom5  10501  brdom4  10502  nqerf  10903  shftfn  15100  2ndcdisj2  23575  plyexmo  26435  ajfuni  31120  funadj  32147  cnlnadjeui  32338  amosym1  36799  sinnpoly  47483  funressnvmo  47637