Theorem confun 41106

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

Hypotheses

Ref	Expression
confun.1	|- ph
confun.2	|- ( ch -> ps )
confun.3	|- ( ch -> th )
confun.4	|- ( ph -> ( ph -> ps ) )

Assertion

Ref	Expression
confun	|- ( ch -> ( th <-> ph ) )

Proof of Theorem confun

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

Syntax hints:   -> wi 4   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  confun2  41107  confun3  41108