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

Theorem biass 349
 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 331 . . . 4
21bibi1d 311 . . 3
3 pm5.501 331 . . 3
42, 3bitr3d 247 . 2
5 nbbn 348 . . . 4
6 nbn2 335 . . . . 5
76bibi1d 311 . . . 4
85, 7syl5bbr 251 . . 3
9 nbn2 335 . . 3
108, 9bitr3d 247 . 2
114, 10pm2.61i 158 1
 Colors of variables: wff set class Syntax hints:   wn 3   wb 177 This theorem is referenced by:  biluk  900  xorass  1317  had1  1411  symdifass  25664 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 178
 Copyright terms: Public domain W3C validator