Theorem moimi 2546

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

Syntax hints:   → wi 4  ∃*wmo 2538

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 2540

This theorem is referenced by:  moa1  2552  moan  2553  moor  2555  mooran1  2556  mooran2  2557  moaneu  2624  2moexv  2628  2euexv  2632  2exeuv  2633  2moex  2641  2euex  2642  2exeu  2647  sndisj  5078  disjxsn  5080  axsepgfromrep  5229  fununmo  6539  funcnvsn  6542  nfunsn  6873  caovmo  7597  iunmapdisj  9936  brdom3  10441  brdom5  10442  brdom4  10443  nqerf  10844  shftfn  15026  2ndcdisj2  23432  plyexmo  26290  ajfuni  30945  funadj  31972  cnlnadjeui  32163  amosym1  36624  sinnpoly  47351  funressnvmo  47505