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

Theorem moimi 2040
Description: "At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 15-Feb-2006.)
Hypothesis
Ref Expression
moimi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
moimi  |-  ( E* x ps  ->  E* x ph )

Proof of Theorem moimi
StepHypRef Expression
1 moim 2039 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E* x ps  ->  E* x ph ) )
2 moimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1410 1  |-  ( E* x ps  ->  E* x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E*wmo 1976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979
This theorem is referenced by:  moan  2044  moor  2046  mooran1  2047  mooran2  2048  2moex  2061  2euex  2062  2exeu  2067  mosubt  2832  sndisj  3893  disjxsn  3895  mosubopt  4572  funcnvsn  5136  nfunsn  5421  th3qlem2  6498  shftfn  10547
  Copyright terms: Public domain W3C validator