Metamath Proof Explorer

Theorem bj-hbxfrbi

Description: Closed form of hbxfrbi . Note: it is less important than nfbiit . The antecedent is in the "strong necessity" modality of modal logic (see also bj-nnftht ) in order not to require sp (modal T). See bj-hbyfrbi for its version with existential quantifiers. (Contributed by BJ, 6-May-2019)

Ref Expression
Assertion bj-hbxfrbi ⊢ φ ↔ ψ ∧ ∀ x φ ↔ ψ → φ → ∀ x φ ↔ ψ → ∀ x ψ

Proof

Step Hyp Ref Expression
1 simpl ⊢ φ ↔ ψ ∧ ∀ x φ ↔ ψ → φ ↔ ψ
2 albi ⊢ ∀ x φ ↔ ψ → ∀ x φ ↔ ∀ x ψ
3 2 adantl ⊢ φ ↔ ψ ∧ ∀ x φ ↔ ψ → ∀ x φ ↔ ∀ x ψ
4 1 3 imbi12d ⊢ φ ↔ ψ ∧ ∀ x φ ↔ ψ → φ → ∀ x φ ↔ ψ → ∀ x ψ