Theorem moimi 2570

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-mo 2564

This theorem is used by:  moa1  2576  moan  2577  moor  2579  mooran1  2580  mooran2  2581  moaneu  2648  2moexv  2652  2euexv  2656  2exeuv  2657  2moex  2665  2euex  2666  2exeu  2671  sndisj  5094  disjxsn  5096  axsepgfromrep  5246  fununmo  6587  funcnvsn  6590  nfunsn  6924  caovmo  7658  iunmapdisj  10105  brdom3  10610  brdom5  10611  brdom4  10612  nqerf  11018  shftfn  15231  2ndcdisj2  23781  plyexmo  26641  ajfuni  31466  funadj  32493  cnlnadjeui  32684  amosym1  37306  sinnpoly  48034  funressnvmo  48208