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

Theorem moimi 2306
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 2305 . 2
2 immoi.1 . 2
31, 2mpg 1588 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E*wmo 2245
This theorem is referenced by:  morimOLD  2307  moan  2311  moor  2313  mooran1  2314  mooran2  2315  moaneu  2322  2moex  2337  2euex  2338  2exeu  2343  2eu1  2347  sndisj  4259  disjxsn  4261  funcnvsn  5433  nfunsn  5691  caovmo  6270  th3qlem2  7168  iunmapdisj  8140  brdom3  8642  brdom5  8643  brdom4  8644  nqerf  9045  shftfn  12503  2ndcdisj2  18765  plyexmo  21520  ajfuni  23939  funadj  24969  cnlnadjeui  25160
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-12 1785
This theorem depends on definitions:  df-bi 179  df-an 364  df-ex 1582  df-nf 1585  df-eu 2248  df-mo 2249
  Copyright terms: Public domain W3C validator