Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rp-fakeimass Structured version   Visualization version   GIF version

Theorem rp-fakeimass 41791
Description: A special case where implication appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.)
Assertion
Ref Expression
rp-fakeimass ((𝜑𝜒) ↔ (((𝜑𝜓) → 𝜒) ↔ (𝜑 → (𝜓𝜒))))

Proof of Theorem rp-fakeimass
StepHypRef Expression
1 pm2.521g 174 . . . . . 6 (¬ (𝜑𝜓) → (𝜓𝜒))
21a1d 25 . . . . 5 (¬ (𝜑𝜓) → (𝜑 → (𝜓𝜒)))
3 ax-1 6 . . . . . 6 (𝜒 → (𝜓𝜒))
43a1d 25 . . . . 5 (𝜒 → (𝜑 → (𝜓𝜒)))
52, 4ja 186 . . . 4 (((𝜑𝜓) → 𝜒) → (𝜑 → (𝜓𝜒)))
6 ax-2 7 . . . . 5 ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → (𝜑𝜒)))
76com3r 87 . . . 4 (𝜑 → ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → 𝜒)))
85, 7impbid2 225 . . 3 (𝜑 → (((𝜑𝜓) → 𝜒) ↔ (𝜑 → (𝜓𝜒))))
9 ax-1 6 . . . 4 (𝜒 → ((𝜑𝜓) → 𝜒))
109, 42thd 265 . . 3 (𝜒 → (((𝜑𝜓) → 𝜒) ↔ (𝜑 → (𝜓𝜒))))
118, 10jaoi 856 . 2 ((𝜑𝜒) → (((𝜑𝜓) → 𝜒) ↔ (𝜑 → (𝜓𝜒))))
12 jarl 125 . . . . 5 (((𝜑𝜓) → 𝜒) → (¬ 𝜑𝜒))
1312orrd 862 . . . 4 (((𝜑𝜓) → 𝜒) → (𝜑𝜒))
1413a1d 25 . . 3 (((𝜑𝜓) → 𝜒) → ((𝜑 → (𝜓𝜒)) → (𝜑𝜒)))
15 simplim 167 . . . . 5 (¬ (𝜑 → (𝜓𝜒)) → 𝜑)
1615orcd 872 . . . 4 (¬ (𝜑 → (𝜓𝜒)) → (𝜑𝜒))
1716a1i 11 . . 3 (¬ ((𝜑𝜓) → 𝜒) → (¬ (𝜑 → (𝜓𝜒)) → (𝜑𝜒)))
1814, 17bija 382 . 2 ((((𝜑𝜓) → 𝜒) ↔ (𝜑 → (𝜓𝜒))) → (𝜑𝜒))
1911, 18impbii 208 1 ((𝜑𝜒) ↔ (((𝜑𝜓) → 𝜒) ↔ (𝜑 → (𝜓𝜒))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wo 846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-or 847
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator