Theorem moimi 2572

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

This proof depends on syntax axioms:   → wi 4  ∃*wmo 2564

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2566

This theorem is used by:  moa1  2578  moan  2579  moor  2581  mooran1  2582  mooran2  2583  moaneu  2650  2moexv  2654  2euexv  2658  2exeuv  2659  2moex  2667  2euex  2668  2exeu  2673  sndisj  5099  disjxsn  5101  axsepgfromrep  5253  fununmo  6584  funcnvsn  6587  nfunsn  6921  caovmo  7655  iunmapdisj  10030  brdom3  10535  brdom5  10536  brdom4  10537  nqerf  10943  shftfn  15150  2ndcdisj2  23689  plyexmo  26552  ajfuni  31348  funadj  32375  cnlnadjeui  32566  amosym1  37053  sinnpoly  47767  funressnvmo  47941