Theorem rp-fakeimass 42725

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

Assertion

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

Proof of Theorem rp-fakeimass

Step	Hyp	Ref	Expression
1		pm2.521g 174	. . . . . 6 ⊢ (¬ (𝜑 → 𝜓) → (𝜓 → 𝜒))
2	1	a1d 25	. . . . 5 ⊢ (¬ (𝜑 → 𝜓) → (𝜑 → (𝜓 → 𝜒)))
3		ax-1 6	. . . . . 6 ⊢ (𝜒 → (𝜓 → 𝜒))
4	3	a1d 25	. . . . 5 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜒)))
5	2, 4	ja 186	. . . 4 ⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
6		ax-2 7	. . . . 5 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
7	6	com3r 87	. . . 4 ⊢ (𝜑 → ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)))
8	5, 7	impbid2 225	. . 3 ⊢ (𝜑 → (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))))
9		ax-1 6	. . . 4 ⊢ (𝜒 → ((𝜑 → 𝜓) → 𝜒))
10	9, 4	2thd 265	. . 3 ⊢ (𝜒 → (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))))
11	8, 10	jaoi 854	. 2 ⊢ ((𝜑 ∨ 𝜒) → (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))))
12		jarl 125	. . . . 5 ⊢ (((𝜑 → 𝜓) → 𝜒) → (¬ 𝜑 → 𝜒))
13	12	orrd 860	. . . 4 ⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜑 ∨ 𝜒))
14	13	a1d 25	. . 3 ⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒)))
15		simplim 167	. . . . 5 ⊢ (¬ (𝜑 → (𝜓 → 𝜒)) → 𝜑)
16	15	orcd 870	. . . 4 ⊢ (¬ (𝜑 → (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒))
17	16	a1i 11	. . 3 ⊢ (¬ ((𝜑 → 𝜓) → 𝜒) → (¬ (𝜑 → (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒)))
18	14, 17	bija 380	. 2 ⊢ ((((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) → (𝜑 ∨ 𝜒))
19	11, 18	impbii 208	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∨ wo 844

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-or 845

This theorem is referenced by: (None)