Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
Axiom scheme ax-4 (Quantified Implication)
2exanali
Next ⟩
exancom
Metamath Proof Explorer
Ascii
Unicode
Theorem
2exanali
Description:
Theorem *11.521 in
WhiteheadRussell
p. 164.
(Contributed by
Andrew Salmon
, 24-May-2011)
Ref
Expression
Assertion
2exanali
⊢
¬
∃
x
∃
y
φ
∧
¬
ψ
↔
∀
x
∀
y
φ
→
ψ
Proof
Step
Hyp
Ref
Expression
1
2nalexn
⊢
¬
∀
x
∀
y
φ
→
ψ
↔
∃
x
∃
y
¬
φ
→
ψ
2
1
con1bii
⊢
¬
∃
x
∃
y
¬
φ
→
ψ
↔
∀
x
∀
y
φ
→
ψ
3
annim
⊢
φ
∧
¬
ψ
↔
¬
φ
→
ψ
4
3
2exbii
⊢
∃
x
∃
y
φ
∧
¬
ψ
↔
∃
x
∃
y
¬
φ
→
ψ
5
2
4
xchnxbir
⊢
¬
∃
x
∃
y
φ
∧
¬
ψ
↔
∀
x
∀
y
φ
→
ψ