Theorem confun5

Description: An attempt at derivative. Resisted simplest path to a proof. Interesting that ch, th, ta, et were all provable. (Contributed by Jarvin Udandy, 7-Sep-2020)

	Ref	Expression
Hypotheses	confun5.1	|- ph
	confun5.2	|- ( ( ph -> ps ) -> ps )
	confun5.3	|- ( ps -> ( ph -> ch ) )
	confun5.4	|- ( ( ch -> th ) -> ( ( ph -> th ) <-> ps ) )
	confun5.5	|- ( ta <-> ( ch -> th ) )
	confun5.6	|- ( et <-> -. ( ch -> ( ch /\ -. ch ) ) )
	confun5.7	|- ps
	confun5.8	|- ( ch -> th )
Assertion	confun5	|- ( ch -> ( et <-> ta ) )

Proof

Step	Hyp	Ref	Expression
1		confun5.1	|- ph
2		confun5.2	|- ( ( ph -> ps ) -> ps )
3		confun5.3	|- ( ps -> ( ph -> ch ) )
4		confun5.4	|- ( ( ch -> th ) -> ( ( ph -> th ) <-> ps ) )
5		confun5.5	|- ( ta <-> ( ch -> th ) )
6		confun5.6	|- ( et <-> -. ( ch -> ( ch /\ -. ch ) ) )
7		confun5.7	|- ps
8		confun5.8	|- ( ch -> th )
9	7 3	ax-mp	|- ( ph -> ch )
10	1 9	ax-mp	|- ch
11	10	atnaiana	|- -. ( ch -> ( ch /\ -. ch ) )
12		bicom1	|- ( ( et <-> -. ( ch -> ( ch /\ -. ch ) ) ) -> ( -. ( ch -> ( ch /\ -. ch ) ) <-> et ) )
13	6 12	ax-mp	|- ( -. ( ch -> ( ch /\ -. ch ) ) <-> et )
14	13	biimpi	|- ( -. ( ch -> ( ch /\ -. ch ) ) -> et )
15	11 14	ax-mp	|- et
16		bicom1	|- ( ( ta <-> ( ch -> th ) ) -> ( ( ch -> th ) <-> ta ) )
17	5 16	ax-mp	|- ( ( ch -> th ) <-> ta )
18	17	biimpi	|- ( ( ch -> th ) -> ta )
19	8 18	ax-mp	|- ta
20	15 19	2th	|- ( et <-> ta )
21		ax-1	|- ( ( et <-> ta ) -> ( ch -> ( et <-> ta ) ) )
22	20 21	ax-mp	|- ( ch -> ( et <-> ta ) )