Theorem moimi 2520

Description: "At most one" 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 2519	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))
2		moimi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1724	1 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑)

Syntax hints:   → wi 4  ∃*wmo 2471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-eu 2474  df-mo 2475

This theorem is referenced by:  moa1  2521  moan  2524  moor  2526  mooran1  2527  mooran2  2528  moaneu  2533  2moex  2543  2euex  2544  2exeu  2549  sndisj  4644  disjxsn  4646  fununmo  5933  funcnvsn  5936  nfunsn  6225  caovmo  6871  iunmapdisj  8846  brdom3  9350  brdom5  9351  brdom4  9352  nqerf  9752  shftfn  13813  2ndcdisj2  21260  plyexmo  24068  ajfuni  27715  funadj  28745  cnlnadjeui  28936