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	⊢ 𝜑
	confun5.2	⊢ ( ( 𝜑 → 𝜓 ) → 𝜓 )
	confun5.3	⊢ ( 𝜓 → ( 𝜑 → 𝜒 ) )
	confun5.4	⊢ ( ( 𝜒 → 𝜃 ) → ( ( 𝜑 → 𝜃 ) ↔ 𝜓 ) )
	confun5.5	⊢ ( 𝜏 ↔ ( 𝜒 → 𝜃 ) )
	confun5.6	⊢ ( 𝜂 ↔ ¬ ( 𝜒 → ( 𝜒 ∧ ¬ 𝜒 ) ) )
	confun5.7	⊢ 𝜓
	confun5.8	⊢ ( 𝜒 → 𝜃 )
Assertion	confun5	⊢ ( 𝜒 → ( 𝜂 ↔ 𝜏 ) )

Proof

Step	Hyp	Ref	Expression
1		confun5.1	⊢ 𝜑
2		confun5.2	⊢ ( ( 𝜑 → 𝜓 ) → 𝜓 )
3		confun5.3	⊢ ( 𝜓 → ( 𝜑 → 𝜒 ) )
4		confun5.4	⊢ ( ( 𝜒 → 𝜃 ) → ( ( 𝜑 → 𝜃 ) ↔ 𝜓 ) )
5		confun5.5	⊢ ( 𝜏 ↔ ( 𝜒 → 𝜃 ) )
6		confun5.6	⊢ ( 𝜂 ↔ ¬ ( 𝜒 → ( 𝜒 ∧ ¬ 𝜒 ) ) )
7		confun5.7	⊢ 𝜓
8		confun5.8	⊢ ( 𝜒 → 𝜃 )
9	7 3	ax-mp	⊢ ( 𝜑 → 𝜒 )
10	1 9	ax-mp	⊢ 𝜒
11	10	atnaiana	⊢ ¬ ( 𝜒 → ( 𝜒 ∧ ¬ 𝜒 ) )
12		bicom1	⊢ ( ( 𝜂 ↔ ¬ ( 𝜒 → ( 𝜒 ∧ ¬ 𝜒 ) ) ) → ( ¬ ( 𝜒 → ( 𝜒 ∧ ¬ 𝜒 ) ) ↔ 𝜂 ) )
13	6 12	ax-mp	⊢ ( ¬ ( 𝜒 → ( 𝜒 ∧ ¬ 𝜒 ) ) ↔ 𝜂 )
14	13	biimpi	⊢ ( ¬ ( 𝜒 → ( 𝜒 ∧ ¬ 𝜒 ) ) → 𝜂 )
15	11 14	ax-mp	⊢ 𝜂
16		bicom1	⊢ ( ( 𝜏 ↔ ( 𝜒 → 𝜃 ) ) → ( ( 𝜒 → 𝜃 ) ↔ 𝜏 ) )
17	5 16	ax-mp	⊢ ( ( 𝜒 → 𝜃 ) ↔ 𝜏 )
18	17	biimpi	⊢ ( ( 𝜒 → 𝜃 ) → 𝜏 )
19	8 18	ax-mp	⊢ 𝜏
20	15 19	2th	⊢ ( 𝜂 ↔ 𝜏 )
21		ax-1	⊢ ( ( 𝜂 ↔ 𝜏 ) → ( 𝜒 → ( 𝜂 ↔ 𝜏 ) ) )
22	20 21	ax-mp	⊢ ( 𝜒 → ( 𝜂 ↔ 𝜏 ) )