Theorem confun4

Description: An attempt at derivative. Resisted simplest path to a proof. (Contributed by Jarvin Udandy, 6-Sep-2020)

	Ref	Expression
Hypotheses	confun4.1	⊢ 𝜑
	confun4.2	⊢ ( ( 𝜑 → 𝜓 ) → 𝜓 )
	confun4.3	⊢ ( 𝜓 → ( 𝜑 → 𝜒 ) )
	confun4.4	⊢ ( ( 𝜒 → 𝜃 ) → ( ( 𝜑 → 𝜃 ) ↔ 𝜓 ) )
	confun4.5	⊢ ( 𝜏 ↔ ( 𝜒 → 𝜃 ) )
	confun4.6	⊢ ( 𝜂 ↔ ¬ ( 𝜒 → ( 𝜒 ∧ ¬ 𝜒 ) ) )
	confun4.7	⊢ 𝜓
	confun4.8	⊢ ( 𝜒 → 𝜃 )
Assertion	confun4	⊢ ( 𝜒 → ( 𝜓 → 𝜏 ) )

Proof

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