Theorem fordisxex 14291

Description: If (ph \/ ps) is true for all x and ps is not true for all x then ph is true for some x.

Assertion

Ref	Expression
fordisxex	|- ((A.x e. A (ph \/ ps) /\ -. A.x e. A ps) -> E.x e. A ph)

Proof of Theorem fordisxex

Step	Hyp	Ref	Expression
1		r19.29 2227	. . 3 |- ((A.x e. A (ph \/ ps) /\ E.x e. A -. ps) -> E.x e. A ((ph \/ ps) /\ -. ps))
2		pm5.61 496	. . . . 5 |- (((ph \/ ps) /\ -. ps) <-> (ph /\ -. ps))
3	2	simplbi 349	. . . 4 |- (((ph \/ ps) /\ -. ps) -> ph)
4	3	reximi 2198	. . 3 |- (E.x e. A ((ph \/ ps) /\ -. ps) -> E.x e. A ph)
5	1, 4	syl 12	. 2 |- ((A.x e. A (ph \/ ps) /\ E.x e. A -. ps) -> E.x e. A ph)
6		rexnal 2114	. 2 |- (E.x e. A -. ps <-> -. A.x e. A ps)
7	5, 6	sylan2br 502	1 |- ((A.x e. A (ph \/ ps) /\ -. A.x e. A ps) -> E.x e. A ph)

Syntax hints:  -. wn 2   -> wi 3   \/ wo 239   /\ wa 240  A.wral 2105  E.wrex 2106

This theorem is referenced by:  intartar 15255

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-ral 2109  df-rex 2110

Copyright terms: Public domain