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

Metamath Proof Explorer

Theorem nanbi2d

Description: Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018)

		Ref	Expression
	Hypothesis	nanbid.1	$⊢ φ \to (ψ \leftrightarrow χ)$
	Assertion	nanbi2d	$⊢ φ \to ((θ ⊼ ψ) \leftrightarrow (θ ⊼ χ))$

Step	Hyp	Ref	Expression
1		nanbid.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2		nanbi2	$⊢ (ψ \leftrightarrow χ) \to ((θ ⊼ ψ) \leftrightarrow (θ ⊼ χ))$
3	1 2	syl	$⊢ φ \to ((θ ⊼ ψ) \leftrightarrow (θ ⊼ χ))$