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

Theorem biass 389
 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 370 . . . 4 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21bibi1d 347 . . 3 (𝜑 → ((𝜓𝜒) ↔ ((𝜑𝜓) ↔ 𝜒)))
3 pm5.501 370 . . 3 (𝜑 → ((𝜓𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
42, 3bitr3d 284 . 2 (𝜑 → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
5 nbbn 388 . . . 4 ((¬ 𝜓𝜒) ↔ ¬ (𝜓𝜒))
6 nbn2 374 . . . . 5 𝜑 → (¬ 𝜓 ↔ (𝜑𝜓)))
76bibi1d 347 . . . 4 𝜑 → ((¬ 𝜓𝜒) ↔ ((𝜑𝜓) ↔ 𝜒)))
85, 7bitr3id 288 . . 3 𝜑 → (¬ (𝜓𝜒) ↔ ((𝜑𝜓) ↔ 𝜒)))
9 nbn2 374 . . 3 𝜑 → (¬ (𝜓𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
108, 9bitr3d 284 . 2 𝜑 → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
114, 10pm2.61i 185 1 (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209 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 210 This theorem is referenced by:  biluk  390  xorass  1508  had1  1606  wl-3xorbi2  35207
 Copyright terms: Public domain W3C validator