Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
Axiom scheme ax-6 (Existence)
19.2d
Next ⟩
19.8w
Metamath Proof Explorer
Ascii
Unicode
Theorem
19.2d
Description:
Deduction associated with
19.2
.
(Contributed by
BJ
, 12-May-2019)
Ref
Expression
Hypothesis
19.2d.1
⊢
φ
→
∀
x
ψ
Assertion
19.2d
⊢
φ
→
∃
x
ψ
Proof
Step
Hyp
Ref
Expression
1
19.2d.1
⊢
φ
→
∀
x
ψ
2
19.2
⊢
∀
x
ψ
→
∃
x
ψ
3
1
2
syl
⊢
φ
→
∃
x
ψ