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	⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) → ( ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ( 𝜓 → ∀ 𝑥 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) → ( 𝜑 ↔ 𝜓 ) )
2		albi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝜓 ) )
3	2	adantl	⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝜓 ) )
4	1 3	imbi12d	⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) → ( ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ( 𝜓 → ∀ 𝑥 𝜓 ) ) )