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	⊢ 𝜑
	confun.2	⊢ ( 𝜒 → 𝜓 )
	confun.3	⊢ ( 𝜒 → 𝜃 )
	confun.4	⊢ ( 𝜑 → ( 𝜑 → 𝜓 ) )
Assertion	confun	⊢ ( 𝜒 → ( 𝜃 ↔ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		confun.1	⊢ 𝜑
2		confun.2	⊢ ( 𝜒 → 𝜓 )
3		confun.3	⊢ ( 𝜒 → 𝜃 )
4		confun.4	⊢ ( 𝜑 → ( 𝜑 → 𝜓 ) )
5		ax-1	⊢ ( 𝜒 → ( 𝜃 → 𝜒 ) )
6	3	a1i	⊢ ( 𝜒 → ( 𝜒 → 𝜃 ) )
7	5 6	impbid	⊢ ( 𝜒 → ( 𝜃 ↔ 𝜒 ) )
8	1 4	ax-mp	⊢ ( 𝜑 → 𝜓 )
9		ax-1	⊢ ( 𝜑 → ( 𝜓 → 𝜑 ) )
10	1 9	ax-mp	⊢ ( 𝜓 → 𝜑 )
11	8 10	impbii	⊢ ( 𝜑 ↔ 𝜓 )
12	2 11	sylibr	⊢ ( 𝜒 → 𝜑 )
13	12	a1i	⊢ ( 𝜒 → ( 𝜒 → 𝜑 ) )
14		ax-1	⊢ ( 𝜒 → ( 𝜑 → 𝜒 ) )
15	13 14	impbid	⊢ ( 𝜒 → ( 𝜒 ↔ 𝜑 ) )
16	7 15	bitrd	⊢ ( 𝜒 → ( 𝜃 ↔ 𝜑 ) )