Theorem nanbi1

Description: Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by Anthony Hart, 1-Sep-2011) (Proof shortened by Wolf Lammen, 27-Jun-2020)

	Ref	Expression
Assertion	nanbi1	$$⊢\left(\phi \leftrightarrow \psi \right)\to \left(\left(\phi ⊼\chi \right)\leftrightarrow \left(\psi ⊼\chi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		imbi1	$$⊢\left(\phi \leftrightarrow \psi \right)\to \left(\left(\phi \to \neg \chi \right)\leftrightarrow \left(\psi \to \neg \chi \right)\right)$$
2		dfnan2	$$⊢\left(\phi ⊼\chi \right)\leftrightarrow \left(\phi \to \neg \chi \right)$$
3		dfnan2	$$⊢\left(\psi ⊼\chi \right)\leftrightarrow \left(\psi \to \neg \chi \right)$$
4	1 2 3	3bitr4g	$$⊢\left(\phi \leftrightarrow \psi \right)\to \left(\left(\phi ⊼\chi \right)\leftrightarrow \left(\psi ⊼\chi \right)\right)$$