Theorem immoi 1411

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

Syntax hints:   -> wi 3  E*wmo 1374

This theorem is referenced by:  moan 1415  moor 1417  2moex 1433  2exeu 1439  2eu1 1442  fvex 3717  caoprmo 4056  th3qlem2 4299  brdom3 4773  brdom5 4774  brdom4 4775  ajfuni 8451  funadj 9730  cnlnadjeu 9925

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376

Copyright terms: Public domain