# 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 ${⊢}\left({\phi }\vee {\chi }\right)↔\left(\left(\left({\phi }\to {\psi }\right)\to {\chi }\right)↔\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 conax1 ${⊢}¬\left({\phi }\to {\psi }\right)\to ¬{\psi }$
2 1 pm2.21d ${⊢}¬\left({\phi }\to {\psi }\right)\to \left({\psi }\to {\chi }\right)$
3 2 a1d ${⊢}¬\left({\phi }\to {\psi }\right)\to \left({\phi }\to \left({\psi }\to {\chi }\right)\right)$
4 ax-1 ${⊢}{\chi }\to \left({\psi }\to {\chi }\right)$
5 4 a1d ${⊢}{\chi }\to \left({\phi }\to \left({\psi }\to {\chi }\right)\right)$
6 3 5 ja ${⊢}\left(\left({\phi }\to {\psi }\right)\to {\chi }\right)\to \left({\phi }\to \left({\psi }\to {\chi }\right)\right)$
7 ax-2 ${⊢}\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to \left({\phi }\to {\chi }\right)\right)$
8 7 com3r ${⊢}{\phi }\to \left(\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to {\chi }\right)\right)$
9 6 8 impbid2 ${⊢}{\phi }\to \left(\left(\left({\phi }\to {\psi }\right)\to {\chi }\right)↔\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\right)$
10 ax-1 ${⊢}{\chi }\to \left(\left({\phi }\to {\psi }\right)\to {\chi }\right)$
11 10 5 2thd ${⊢}{\chi }\to \left(\left(\left({\phi }\to {\psi }\right)\to {\chi }\right)↔\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\right)$
12 9 11 jaoi ${⊢}\left({\phi }\vee {\chi }\right)\to \left(\left(\left({\phi }\to {\psi }\right)\to {\chi }\right)↔\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\right)$
13 jarl ${⊢}\left(\left({\phi }\to {\psi }\right)\to {\chi }\right)\to \left(¬{\phi }\to {\chi }\right)$
14 13 orrd ${⊢}\left(\left({\phi }\to {\psi }\right)\to {\chi }\right)\to \left({\phi }\vee {\chi }\right)$
15 14 a1d ${⊢}\left(\left({\phi }\to {\psi }\right)\to {\chi }\right)\to \left(\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\to \left({\phi }\vee {\chi }\right)\right)$
16 simplim ${⊢}¬\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\to {\phi }$
17 16 orcd ${⊢}¬\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\to \left({\phi }\vee {\chi }\right)$
18 17 a1i ${⊢}¬\left(\left({\phi }\to {\psi }\right)\to {\chi }\right)\to \left(¬\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\to \left({\phi }\vee {\chi }\right)\right)$
19 15 18 bija ${⊢}\left(\left(\left({\phi }\to {\psi }\right)\to {\chi }\right)↔\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\right)\to \left({\phi }\vee {\chi }\right)$
20 12 19 impbii ${⊢}\left({\phi }\vee {\chi }\right)↔\left(\left(\left({\phi }\to {\psi }\right)\to {\chi }\right)↔\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\right)$