Theorem moimi 2549

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

Syntax hints:   → wi 4  ∃*wmo 2541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-mo 2543

This theorem is referenced by:  moa1  2555  moan  2556  moor  2558  mooran1  2559  mooran2  2560  moaneu  2627  2moexv  2631  2euexv  2635  2exeuv  2636  2moex  2644  2euex  2645  2exeu  2650  sndisj  5071  disjxsn  5073  axsepgfromrep  5223  fununmo  6539  funcnvsn  6542  nfunsn  6873  caovmo  7600  iunmapdisj  9943  brdom3  10448  brdom5  10449  brdom4  10450  nqerf  10851  shftfn  15033  2ndcdisj2  23447  plyexmo  26304  ajfuni  30955  funadj  31982  cnlnadjeui  32173  amosym1  36661  sinnpoly  47361  funressnvmo  47515