Theorem confun4 44324

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

Hypotheses

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

Assertion

Ref	Expression
confun4	⊢ (𝜒 → (𝜓 → 𝜏))

Proof of Theorem confun4

Step	Hyp	Ref	Expression
1		confun4.1	. . . 4 ⊢ 𝜑
2		confun4.7	. . . . 5 ⊢ 𝜓
3		confun4.3	. . . . 5 ⊢ (𝜓 → (𝜑 → 𝜒))
4	2, 3	ax-mp 5	. . . 4 ⊢ (𝜑 → 𝜒)
5	1, 4	ax-mp 5	. . 3 ⊢ 𝜒
6		confun4.8	. . . . . 6 ⊢ (𝜒 → 𝜃)
7		confun4.5	. . . . . . . 8 ⊢ (𝜏 ↔ (𝜒 → 𝜃))
8		bicom1 220	. . . . . . . 8 ⊢ ((𝜏 ↔ (𝜒 → 𝜃)) → ((𝜒 → 𝜃) ↔ 𝜏))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ((𝜒 → 𝜃) ↔ 𝜏)
10	9	biimpi 215	. . . . . 6 ⊢ ((𝜒 → 𝜃) → 𝜏)
11	6, 10	ax-mp 5	. . . . 5 ⊢ 𝜏
12	2, 11	pm3.2i 470	. . . 4 ⊢ (𝜓 ∧ 𝜏)
13		pm3.4 806	. . . 4 ⊢ ((𝜓 ∧ 𝜏) → (𝜓 → 𝜏))
14	12, 13	ax-mp 5	. . 3 ⊢ (𝜓 → 𝜏)
15	5, 14	pm3.2i 470	. 2 ⊢ (𝜒 ∧ (𝜓 → 𝜏))
16		pm3.4 806	. 2 ⊢ ((𝜒 ∧ (𝜓 → 𝜏)) → (𝜒 → (𝜓 → 𝜏)))
17	15, 16	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

This theorem is referenced by: (None)