Metamath Proof Explorer

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 conax1 ⊢ ( ¬ ( 𝜑 → 𝜓 ) → ¬ 𝜓 )
2 1 pm2.21d ⊢ ( ¬ ( 𝜑 → 𝜓 ) → ( 𝜓 → 𝜒 ) )
3 2 a1d ⊢ ( ¬ ( 𝜑 → 𝜓 ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) )
4 ax-1 ⊢ ( 𝜒 → ( 𝜓 → 𝜒 ) )
5 4 a1d ⊢ ( 𝜒 → ( 𝜑 → ( 𝜓 → 𝜒 ) ) )
6 3 5 ja ⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) )
7 ax-2 ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜒 ) ) )
8 7 com3r ⊢ ( 𝜑 → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( 𝜑 → 𝜓 ) → 𝜒 ) ) )
9 6 8 impbid2 ⊢ ( 𝜑 → ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) )
10 ax-1 ⊢ ( 𝜒 → ( ( 𝜑 → 𝜓 ) → 𝜒 ) )
11 10 5 2thd ⊢ ( 𝜒 → ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) )
12 9 11 jaoi ⊢ ( ( 𝜑 ∨ 𝜒 ) → ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) )
13 jarl ⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( ¬ 𝜑 → 𝜒 ) )
14 13 orrd ⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( 𝜑 ∨ 𝜒 ) )
15 14 a1d ⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 ∨ 𝜒 ) ) )
16 simplim ⊢ ( ¬ ( 𝜑 → ( 𝜓 → 𝜒 ) ) → 𝜑 )
17 16 orcd ⊢ ( ¬ ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 ∨ 𝜒 ) )
18 17 a1i ⊢ ( ¬ ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( ¬ ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 ∨ 𝜒 ) ) )
19 15 18 bija ⊢ ( ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( 𝜑 ∨ 𝜒 ) )
20 12 19 impbii ⊢ ( ( 𝜑 ∨ 𝜒 ) ↔ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) )