Theorem alimp-no-surprise

Description: There is no "surprise" in a for-all with implication if there exists a value where the antecedent is true. This is one way to prevent for-all with implication from allowing anything. For a contrast, see alimp-surprise . The allsome quantifier also counters this problem, see df-alsi . (Contributed by David A. Wheeler, 27-Oct-2018)

	Ref	Expression
Assertion	alimp-no-surprise	|- -. ( A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) /\ E. x ph )

Proof

Step	Hyp	Ref	Expression
1		pm4.82	|- ( ( ( ph -> ps ) /\ ( ph -> -. ps ) ) <-> -. ph )
2	1	albii	|- ( A. x ( ( ph -> ps ) /\ ( ph -> -. ps ) ) <-> A. x -. ph )
3		alnex	|- ( A. x -. ph <-> -. E. x ph )
4	2 3	sylbb	|- ( A. x ( ( ph -> ps ) /\ ( ph -> -. ps ) ) -> -. E. x ph )
5		imnan	|- ( ( A. x ( ( ph -> ps ) /\ ( ph -> -. ps ) ) -> -. E. x ph ) <-> -. ( A. x ( ( ph -> ps ) /\ ( ph -> -. ps ) ) /\ E. x ph ) )
6	4 5	mpbi	|- -. ( A. x ( ( ph -> ps ) /\ ( ph -> -. ps ) ) /\ E. x ph )
7		19.26	|- ( A. x ( ( ph -> ps ) /\ ( ph -> -. ps ) ) <-> ( A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) ) )
8	7	anbi2ci	|- ( ( A. x ( ( ph -> ps ) /\ ( ph -> -. ps ) ) /\ E. x ph ) <-> ( E. x ph /\ ( A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) ) ) )
9		3anass	|- ( ( E. x ph /\ A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) ) <-> ( E. x ph /\ ( A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) ) ) )
10		3anrot	|- ( ( E. x ph /\ A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) ) <-> ( A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) /\ E. x ph ) )
11	8 9 10	3bitr2i	|- ( ( A. x ( ( ph -> ps ) /\ ( ph -> -. ps ) ) /\ E. x ph ) <-> ( A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) /\ E. x ph ) )
12	6 11	mtbi	|- -. ( A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) /\ E. x ph )