Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
Rule scheme ax-gen (Generalization)
gen2
Next ⟩
mpg
Metamath Proof Explorer
Ascii
Structured
Theorem
gen2
Description:
Generalization applied twice.
(Contributed by
NM
, 30-Apr-1998)
Ref
Expression
Hypothesis
gen2.1
⊢
𝜑
Assertion
gen2
⊢
∀
𝑥
∀
𝑦
𝜑
Proof
Step
Hyp
Ref
Expression
1
gen2.1
⊢
𝜑
2
1
ax-gen
⊢
∀
𝑦
𝜑
3
2
ax-gen
⊢
∀
𝑥
∀
𝑦
𝜑