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

Theorem moimi 2330
 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 2329 . 2
2 immoi.1 . 2
31, 2mpg 1558 1
 Colors of variables: wff set class Syntax hints:   wi 4  wmo 2284 This theorem is referenced by:  moan  2334  moor  2336  mooran1  2337  mooran2  2338  2moex  2354  2euex  2355  2exeu  2360  2eu1  2363  sndisj  4206  disjxsn  4208  funcnvsn  5498  nfunsn  5763  caovmo  6286  th3qlem2  7013  iunmapdisj  7906  brdom3  8408  brdom5  8409  brdom4  8410  nqerf  8809  shftfn  11890  2ndcdisj2  17522  plyexmo  20232  ajfuni  22363  funadj  23391  cnlnadjeui  23582 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288
 Copyright terms: Public domain W3C validator