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	|- ph
	confun.2	|- ( ch -> ps )
	confun.3	|- ( ch -> th )
	confun.4	|- ( ph -> ( ph -> ps ) )
Assertion	confun	|- ( ch -> ( th <-> ph ) )

Proof

Step	Hyp	Ref	Expression
1		confun.1	|- ph
2		confun.2	|- ( ch -> ps )
3		confun.3	|- ( ch -> th )
4		confun.4	|- ( ph -> ( ph -> ps ) )
5		ax-1	|- ( ch -> ( th -> ch ) )
6	3	a1i	|- ( ch -> ( ch -> th ) )
7	5 6	impbid	|- ( ch -> ( th <-> ch ) )
8	1 4	ax-mp	|- ( ph -> ps )
9		ax-1	|- ( ph -> ( ps -> ph ) )
10	1 9	ax-mp	|- ( ps -> ph )
11	8 10	impbii	|- ( ph <-> ps )
12	2 11	sylibr	|- ( ch -> ph )
13	12	a1i	|- ( ch -> ( ch -> ph ) )
14		ax-1	|- ( ch -> ( ph -> ch ) )
15	13 14	impbid	|- ( ch -> ( ch <-> ph ) )
16	7 15	bitrd	|- ( ch -> ( th <-> ph ) )