Theorem rp-fakeimass

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

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

Proof

Step	Hyp	Ref	Expression
1		pm2.521g	⊢ ( ¬ ( 𝜑 → 𝜓 ) → ( 𝜓 → 𝜒 ) )
2	1	a1d	⊢ ( ¬ ( 𝜑 → 𝜓 ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) )
3		ax-1	⊢ ( 𝜒 → ( 𝜓 → 𝜒 ) )
4	3	a1d	⊢ ( 𝜒 → ( 𝜑 → ( 𝜓 → 𝜒 ) ) )
5	2 4	ja	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) )
6		ax-2	⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜒 ) ) )
7	6	com3r	⊢ ( 𝜑 → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( 𝜑 → 𝜓 ) → 𝜒 ) ) )
8	5 7	impbid2	⊢ ( 𝜑 → ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) )
9		ax-1	⊢ ( 𝜒 → ( ( 𝜑 → 𝜓 ) → 𝜒 ) )
10	9 4	2thd	⊢ ( 𝜒 → ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) )
11	8 10	jaoi	⊢ ( ( 𝜑 ∨ 𝜒 ) → ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) )
12		jarl	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( ¬ 𝜑 → 𝜒 ) )
13	12	orrd	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( 𝜑 ∨ 𝜒 ) )
14	13	a1d	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 ∨ 𝜒 ) ) )
15		simplim	⊢ ( ¬ ( 𝜑 → ( 𝜓 → 𝜒 ) ) → 𝜑 )
16	15	orcd	⊢ ( ¬ ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 ∨ 𝜒 ) )
17	16	a1i	⊢ ( ¬ ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( ¬ ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 ∨ 𝜒 ) ) )
18	14 17	bija	⊢ ( ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( 𝜑 ∨ 𝜒 ) )
19	11 18	impbii	⊢ ( ( 𝜑 ∨ 𝜒 ) ↔ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) )