Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  moimi GIF version

Theorem moimi 1965
 Description: "At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 15-Feb-2006.)
Hypothesis
Ref Expression
moimi.1 (𝜑𝜓)
Assertion
Ref Expression
moimi (∃*𝑥𝜓 → ∃*𝑥𝜑)

Proof of Theorem moimi
StepHypRef Expression
1 moim 1964 . 2 (∀𝑥(𝜑𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))
2 moimi.1 . 2 (𝜑𝜓)
31, 2mpg 1340 1 (∃*𝑥𝜓 → ∃*𝑥𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∃*wmo 1901 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904 This theorem is referenced by:  moan  1969  moor  1971  mooran1  1972  mooran2  1973  2moex  1986  2euex  1987  2exeu  1992  mosubt  2718  sndisj  3760  disjxsn  3762  mosubopt  4405  funcnvsn  4945  nfunsn  5207  th3qlem2  6209  shftfn  9425
 Copyright terms: Public domain W3C validator