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 φ χ φ ψ χ φ ψ χ