Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-bixor Structured version   Visualization version   GIF version

Theorem bj-bixor 34769
Description: Equivalence of two ternary operations. Note the identical order and parenthesizing of the three arguments in both expressions. (Contributed by BJ, 31-Dec-2023.)
Assertion
Ref Expression
bj-bixor ((𝜑 ↔ (𝜓𝜒)) ↔ (𝜑 ⊻ (𝜓𝜒)))

Proof of Theorem bj-bixor
StepHypRef Expression
1 pm5.18 383 . . 3 ((𝜑 ↔ (𝜓𝜒)) ↔ ¬ (𝜑 ↔ ¬ (𝜓𝜒)))
21con2bii 358 . 2 ((𝜑 ↔ ¬ (𝜓𝜒)) ↔ ¬ (𝜑 ↔ (𝜓𝜒)))
3 df-xor 1507 . . 3 ((𝜓𝜒) ↔ ¬ (𝜓𝜒))
43bibi2i 338 . 2 ((𝜑 ↔ (𝜓𝜒)) ↔ (𝜑 ↔ ¬ (𝜓𝜒)))
5 df-xor 1507 . 2 ((𝜑 ⊻ (𝜓𝜒)) ↔ ¬ (𝜑 ↔ (𝜓𝜒)))
62, 4, 53bitr4i 303 1 ((𝜑 ↔ (𝜓𝜒)) ↔ (𝜑 ⊻ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wxo 1506
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-xor 1507
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator