Theorem immoi 2079

Description: "At most one" is preserved through implication (notice wff reversal).

Hypothesis

Ref	Expression
immoi.1	|- (ph -> ps)

Assertion

Ref	Expression
immoi	|- (E*xps -> E*xph)

Proof of Theorem immoi

Step	Hyp	Ref	Expression
1		immo 2078	. 2 |- (A.x(ph -> ps) -> (E*xps -> E*xph))
2		immoi.1	. 2 |- (ph -> ps)
3	1, 2	mpg 1621	1 |- (E*xps -> E*xph)

Syntax hints:   -> wi 3  E*wmo 2038

This theorem is referenced by:  moan 2083  moor 2085  mooran1 2086  mooran2 2087  2moex 2103  2euex 2104  2exeu 2109  2eu1 2112  fvex 4778  nfunsn 4792  caoprmo 5096  th3qlem2 5535  brdom3 6377  brdom5 6378  brdom4 6379  ajfuni 10730  funadj 12282  cnlnadjeui 12479

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042

Copyright terms: Public domain