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