Theorem rp-fakeimass 38815

Description: A special case where implication appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)

Assertion

Ref	Expression
rp-fakeimass	⊢ ((𝜑 ∨ 𝜒) ↔ (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))))

Proof of Theorem rp-fakeimass

Step	Hyp	Ref	Expression
1		ax-1 6	. . . . . . . 8 ⊢ (𝜓 → (𝜑 → 𝜓))
2	1	con3i 152	. . . . . . 7 ⊢ (¬ (𝜑 → 𝜓) → ¬ 𝜓)
3	2	pm2.21d 119	. . . . . 6 ⊢ (¬ (𝜑 → 𝜓) → (𝜓 → 𝜒))
4	3	a1d 25	. . . . 5 ⊢ (¬ (𝜑 → 𝜓) → (𝜑 → (𝜓 → 𝜒)))
5		ax-1 6	. . . . . 6 ⊢ (𝜒 → (𝜓 → 𝜒))
6	5	a1d 25	. . . . 5 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜒)))
7	4, 6	ja 175	. . . 4 ⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
8		ax-2 7	. . . . 5 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
9	8	com3r 87	. . . 4 ⊢ (𝜑 → ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)))
10	7, 9	impbid2 218	. . 3 ⊢ (𝜑 → (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))))
11		ax-1 6	. . . 4 ⊢ (𝜒 → ((𝜑 → 𝜓) → 𝜒))
12	11, 6	2thd 257	. . 3 ⊢ (𝜒 → (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))))
13	10, 12	jaoi 846	. 2 ⊢ ((𝜑 ∨ 𝜒) → (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))))
14		jarl 123	. . . . 5 ⊢ (((𝜑 → 𝜓) → 𝜒) → (¬ 𝜑 → 𝜒))
15	14	orrd 852	. . . 4 ⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜑 ∨ 𝜒))
16	15	a1d 25	. . 3 ⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒)))
17		simplim 165	. . . . 5 ⊢ (¬ (𝜑 → (𝜓 → 𝜒)) → 𝜑)
18	17	orcd 862	. . . 4 ⊢ (¬ (𝜑 → (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒))
19	18	a1i 11	. . 3 ⊢ (¬ ((𝜑 → 𝜓) → 𝜒) → (¬ (𝜑 → (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒)))
20	16, 19	bija 372	. 2 ⊢ ((((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) → (𝜑 ∨ 𝜒))
21	13, 20	impbii 201	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∨ wo 836

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 199  df-or 837

This theorem is referenced by: (None)