Theorem confun

Description: Given the hypotheses there exists a proof for (c implies ( d iff a ) ). (Contributed by Jarvin Udandy, 6-Sep-2020)

	Ref	Expression
Hypotheses	confun.1	$$⊢\phi$$
	confun.2	$$⊢\chi \to \psi$$
	confun.3	$$⊢\chi \to \theta$$
	confun.4	$$⊢\phi \to \left(\phi \to \psi \right)$$
Assertion	confun	$$⊢\chi \to \left(\theta \leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		confun.1	$$⊢\phi$$
2		confun.2	$$⊢\chi \to \psi$$
3		confun.3	$$⊢\chi \to \theta$$
4		confun.4	$$⊢\phi \to \left(\phi \to \psi \right)$$
5		ax-1	$$⊢\chi \to \left(\theta \to \chi \right)$$
6	3	a1i	$$⊢\chi \to \left(\chi \to \theta \right)$$
7	5 6	impbid	$$⊢\chi \to \left(\theta \leftrightarrow \chi \right)$$
8	1 4	ax-mp	$$⊢\phi \to \psi$$
9		ax-1	$$⊢\phi \to \left(\psi \to \phi \right)$$
10	1 9	ax-mp	$$⊢\psi \to \phi$$
11	8 10	impbii	$$⊢\phi \leftrightarrow \psi$$
12	2 11	sylibr	$$⊢\chi \to \phi$$
13	12	a1i	$$⊢\chi \to \left(\chi \to \phi \right)$$
14		ax-1	$$⊢\chi \to \left(\phi \to \chi \right)$$
15	13 14	impbid	$$⊢\chi \to \left(\chi \leftrightarrow \phi \right)$$
16	7 15	bitrd	$$⊢\chi \to \left(\theta \leftrightarrow \phi \right)$$