Metamath Proof Explorer


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 ¬xφψxφ¬ψxφ

Proof

Step Hyp Ref Expression
1 pm4.82 φψφ¬ψ¬φ
2 1 albii xφψφ¬ψx¬φ
3 alnex x¬φ¬xφ
4 2 3 sylbb xφψφ¬ψ¬xφ
5 imnan xφψφ¬ψ¬xφ¬xφψφ¬ψxφ
6 4 5 mpbi ¬xφψφ¬ψxφ
7 19.26 xφψφ¬ψxφψxφ¬ψ
8 7 anbi2ci xφψφ¬ψxφxφxφψxφ¬ψ
9 3anass xφxφψxφ¬ψxφxφψxφ¬ψ
10 3anrot xφxφψxφ¬ψxφψxφ¬ψxφ
11 8 9 10 3bitr2i xφψφ¬ψxφxφψxφ¬ψxφ
12 6 11 mtbi ¬xφψxφ¬ψxφ