Theorem biadaniALT

Description: Alternate proof of biadani not using biadan . (Contributed by BJ, 4-Mar-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	biadani.1	$$⊢\phi \to \psi$$
Assertion	biadaniALT	$$⊢\left(\psi \to \left(\phi \leftrightarrow \chi \right)\right)\leftrightarrow \left(\phi \leftrightarrow \left(\psi \wedge \chi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		biadani.1	$$⊢\phi \to \psi$$
2		pm5.32	$$⊢\left(\psi \to \left(\phi \leftrightarrow \chi \right)\right)\leftrightarrow \left(\left(\psi \wedge \phi \right)\leftrightarrow \left(\psi \wedge \chi \right)\right)$$
3	1	pm4.71ri	$$⊢\phi \leftrightarrow \left(\psi \wedge \phi \right)$$
4	3	bibi1i	$$⊢\left(\phi \leftrightarrow \left(\psi \wedge \chi \right)\right)\leftrightarrow \left(\left(\psi \wedge \phi \right)\leftrightarrow \left(\psi \wedge \chi \right)\right)$$
5	2 4	bitr4i	$$⊢\left(\psi \to \left(\phi \leftrightarrow \chi \right)\right)\leftrightarrow \left(\phi \leftrightarrow \left(\psi \wedge \chi \right)\right)$$