This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Predicate calculus with equality: Auxiliary axiom schemes (4 schemes) Axiom scheme ax-12 (Substitution) 19.28
Description: Theorem 19.28 of Margaris p. 90. See 19.28v for a version requiring
fewer axioms. (Contributed by NM , 1-Aug-1993) (Proof shortened by Wolf Lammen , 7-May-2025)
Ref
Expression
Hypothesis
19.28.1 ⊢ Ⅎ 𝑥 𝜑
Assertion
19.28 ⊢ ( ∀ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∀ 𝑥 𝜓 ) )
Proof
Step
Hyp
Ref
Expression
1
19.28.1 ⊢ Ⅎ 𝑥 𝜑
2
19.26 ⊢ ( ∀ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) )
3
1
19.3 ⊢ ( ∀ 𝑥 𝜑 ↔ 𝜑 )
4
2 3
bianbi ⊢ ( ∀ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∀ 𝑥 𝜓 ) )