MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  moimi Unicode version

Theorem moimi 2340
Description: "At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 15-Feb-2006.)
Hypothesis
Ref Expression
immoi.1
Assertion
Ref Expression
moimi

Proof of Theorem moimi
StepHypRef Expression
1 moim 2339 . 2
2 immoi.1 . 2
31, 2mpg 1620 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E*wmo 2283
This theorem is referenced by:  morimOLD  2341  moan  2345  moor  2347  mooran1  2348  mooran2  2349  moaneu  2354  2moex  2365  2euex  2366  2exeu  2371  2eu1OLD  2377  sndisj  4444  disjxsn  4446  fununmo  5636  funcnvsn  5638  nfunsn  5902  caovmo  6512  iunmapdisj  8425  brdom3  8927  brdom5  8928  brdom4  8929  nqerf  9329  shftfn  12906  2ndcdisj2  19958  plyexmo  22709  ajfuni  25775  funadj  26805  cnlnadjeui  26996
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-eu 2286  df-mo 2287
  Copyright terms: Public domain W3C validator