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 1799	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 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 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  5077  disjxsn  5079  axsepgfromrep  5229  fununmo  6545  funcnvsn  6548  nfunsn  6879  caovmo  7604  iunmapdisj  9945  brdom3  10450  brdom5  10451  brdom4  10452  nqerf  10853  shftfn  15035  2ndcdisj2  23422  plyexmo  26279  ajfuni  30930  funadj  31957  cnlnadjeui  32148  amosym1  36608  sinnpoly  47339  funressnvmo  47493