Theorem eximp-surprise2

Description: Show that "there exists" with an implication is always true if there exists a situation where the antecedent is false.

Those inexperienced with formal notations of classical logic may use expressions combining "there exists" with implication. This is usually a mistake, because that combination does not mean what an inexperienced person might think it means. For example, if there is some object that does not meet the precondition ph , then the expression E. x ( ph -> ps ) as a whole is always true, no matter what ps is ( ps could even be false, F. ). New users of formal notation who use "there exists" with an implication should consider if they meant "and" instead of "implies". See eximp-surprise , which shows what implication really expands to. See also empty-surprise . (Contributed by David A. Wheeler, 18-Oct-2018)

	Ref	Expression
Hypothesis	eximp-surprise2.1	|- E. x -. ph
Assertion	eximp-surprise2	|- E. x ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		eximp-surprise2.1	|- E. x -. ph
2		orc	|- ( -. ph -> ( -. ph \/ ps ) )
3	1 2	eximii	|- E. x ( -. ph \/ ps )
4		eximp-surprise	|- ( E. x ( ph -> ps ) <-> E. x ( -. ph \/ ps ) )
5	3 4	mpbir	|- E. x ( ph -> ps )