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 ⊢ φ ∨ χ ↔ φ → ψ → χ ↔ φ → ψ → χ