bj-animbi

Description: Conjunction in terms of implication and biconditional. Note that the proof is intuitionistic (use of ax-3 comes from the unusual definition of the biconditional in set.mm). (Contributed by BJ, 23-Sep-2023)

		Ref	Expression
	Assertion	bj-animbi	$⊢ (φ \land ψ) \leftrightarrow (φ \leftrightarrow (φ \to ψ))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (φ \land ψ) \to φ$
2		pm3.4	$⊢ (φ \land ψ) \to (φ \to ψ)$
3	1 2	2thd	$⊢ (φ \land ψ) \to (φ \leftrightarrow (φ \to ψ))$
4		biimp	$⊢ (φ \leftrightarrow (φ \to ψ)) \to (φ \to (φ \to ψ))$
5	4	pm2.43d	$⊢ (φ \leftrightarrow (φ \to ψ)) \to (φ \to ψ)$
6		biimpr	$⊢ (φ \leftrightarrow (φ \to ψ)) \to ((φ \to ψ) \to φ)$
7	5 6	mpd	$⊢ (φ \leftrightarrow (φ \to ψ)) \to φ$
8	7 5	jcai	$⊢ (φ \leftrightarrow (φ \to ψ)) \to (φ \land ψ)$
9	3 8	impbii	$⊢ (φ \land ψ) \leftrightarrow (φ \leftrightarrow (φ \to ψ))$

Metamath Proof Explorer

Theorem bj-animbi

Proof