Theorem immoi 1418

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 1417	. 2 |- (A.x(ph -> ps) -> (E*xps -> E*xph))
2		immoi.1	. 2 |- (ph -> ps)
3	1, 2	mpg 986	1 |- (E*xps -> E*xph)

Syntax hints:   -> wi 3  E*wmo 1381

This theorem is referenced by:  moan 1422  moor 1424  2moex 1440  2exeu 1446  2eu1 1449  fvex 3732  caoprmo 4070  th3qlem2 4315  brdom3 4801  brdom5 4802  brdom4 4803  ajfuni 8520  funadj 9813  cnlnadjeu 10010

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383

Copyright terms: Public domain