MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biass Structured version   Visualization version   GIF version

Theorem biass 386
Description: Associative law for the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs", Annals of Pure and Applied Logic, 113:207-224, 2002, http://www.cs.utexas.edu/users/ai-lab/pub-view.php?PubID=26805. Interestingly, this law was not included in Principia Mathematica but was apparently first noted by Jan Lukasiewicz circa 1923. (Contributed by NM, 8-Jan-2005.) (Proof shortened by Juha Arpiainen, 19-Jan-2006.) (Proof shortened by Wolf Lammen, 21-Sep-2013.)
Assertion
Ref Expression
biass (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒)))

Proof of Theorem biass
StepHypRef Expression
1 pm5.501 368 . . . 4 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21bibi1d 345 . . 3 (𝜑 → ((𝜓𝜒) ↔ ((𝜑𝜓) ↔ 𝜒)))
3 pm5.501 368 . . 3 (𝜑 → ((𝜓𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
42, 3bitr3d 282 . 2 (𝜑 → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
5 nbbn 385 . . . 4 ((¬ 𝜓𝜒) ↔ ¬ (𝜓𝜒))
6 nbn2 372 . . . . 5 𝜑 → (¬ 𝜓 ↔ (𝜑𝜓)))
76bibi1d 345 . . . 4 𝜑 → ((¬ 𝜓𝜒) ↔ ((𝜑𝜓) ↔ 𝜒)))
85, 7syl5bbr 286 . . 3 𝜑 → (¬ (𝜓𝜒) ↔ ((𝜑𝜓) ↔ 𝜒)))
9 nbn2 372 . . 3 𝜑 → (¬ (𝜓𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
108, 9bitr3d 282 . 2 𝜑 → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
114, 10pm2.61i 183 1 (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207
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 208
This theorem is referenced by:  biluk  387  xorass  1499  had1  1595
  Copyright terms: Public domain W3C validator