Theorem confun5 44389

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.)

Hypotheses

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

Assertion

Ref	Expression
confun5	⊢ (𝜒 → (𝜂 ↔ 𝜏))

Proof of Theorem confun5

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395

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 206  df-an 396  df-tru 1544  df-fal 1554

This theorem is referenced by: (None)