This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-ax12ig

Description: A lemma used to prove a weak form of the axiom of substitution. A generalization of bj-ax12i . (Contributed by BJ, 19-Dec-2020)

Ref Expression
Hypotheses bj-ax12ig.1 ⊢ φ → ψ ↔ χ
bj-ax12ig.2 ⊢ φ → χ → ∀ x χ
Assertion bj-ax12ig ⊢ φ → ψ → ∀ x φ → ψ

Proof

Step Hyp Ref Expression
1 bj-ax12ig.1 ⊢ φ → ψ ↔ χ
2 bj-ax12ig.2 ⊢ φ → χ → ∀ x χ
3 1 pm5.32i ⊢ φ ∧ ψ ↔ φ ∧ χ
4 2 imp ⊢ φ ∧ χ → ∀ x χ
5 1 biimprcd ⊢ χ → φ → ψ
6 4 5 sylg ⊢ φ ∧ χ → ∀ x φ → ψ
7 3 6 sylbi ⊢ φ ∧ ψ → ∀ x φ → ψ
8 7 ex ⊢ φ → ψ → ∀ x φ → ψ