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

Theorem moimi 2373
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 2372 . 2
2 immoi.1 . 2
31, 2mpg 1572 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  E*wmo 2314
This theorem is referenced by:  morimOLD  2374  moan  2378  moor  2380  mooran1  2381  mooran2  2382  moaneu  2389  2moex  2404  2euex  2405  2exeu  2410  2eu1  2414  sndisj  4310  disjxsn  4312  funcnvsn  5481  nfunsn  5737  caovmo  6310  th3qlem2  7173  iunmapdisj  8075  brdom3  8577  brdom5  8578  brdom4  8579  nqerf  8978  shftfn  12409  2ndcdisj2  18535  plyexmo  21245  ajfuni  23382  funadj  24412  cnlnadjeui  24603
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1338  df-ex 1566  df-nf 1569  df-eu 2317  df-mo 2318
  Copyright terms: Public domain W3C validator