New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  biass GIF version

Theorem biass 348
 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 330 . . . 4 (φ → (ψ ↔ (φψ)))
21bibi1d 310 . . 3 (φ → ((ψχ) ↔ ((φψ) ↔ χ)))
3 pm5.501 330 . . 3 (φ → ((ψχ) ↔ (φ ↔ (ψχ))))
42, 3bitr3d 246 . 2 (φ → (((φψ) ↔ χ) ↔ (φ ↔ (ψχ))))
5 nbbn 347 . . . 4 ((¬ ψχ) ↔ ¬ (ψχ))
6 nbn2 334 . . . . 5 φ → (¬ ψ ↔ (φψ)))
76bibi1d 310 . . . 4 φ → ((¬ ψχ) ↔ ((φψ) ↔ χ)))
85, 7syl5bbr 250 . . 3 φ → (¬ (ψχ) ↔ ((φψ) ↔ χ)))
9 nbn2 334 . . 3 φ → (¬ (ψχ) ↔ (φ ↔ (ψχ))))
108, 9bitr3d 246 . 2 φ → (((φψ) ↔ χ) ↔ (φ ↔ (ψχ))))
114, 10pm2.61i 156 1 (((φψ) ↔ χ) ↔ (φ ↔ (ψχ)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 176 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177 This theorem is referenced by:  biluk  899  xorass  1308  had1  1402
 Copyright terms: Public domain W3C validator