Theorem 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	|- ( ( ph /\ ps ) <-> ( ph <-> ( ph -> ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( ph /\ ps ) -> ph )
2		pm3.4	|- ( ( ph /\ ps ) -> ( ph -> ps ) )
3	1 2	2thd	|- ( ( ph /\ ps ) -> ( ph <-> ( ph -> ps ) ) )
4		biimp	|- ( ( ph <-> ( ph -> ps ) ) -> ( ph -> ( ph -> ps ) ) )
5	4	pm2.43d	|- ( ( ph <-> ( ph -> ps ) ) -> ( ph -> ps ) )
6		biimpr	|- ( ( ph <-> ( ph -> ps ) ) -> ( ( ph -> ps ) -> ph ) )
7	5 6	mpd	|- ( ( ph <-> ( ph -> ps ) ) -> ph )
8	7 5	jcai	|- ( ( ph <-> ( ph -> ps ) ) -> ( ph /\ ps ) )
9	3 8	impbii	|- ( ( ph /\ ps ) <-> ( ph <-> ( ph -> ps ) ) )