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

Theorem biass 360
 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 342 . . . 4
21bibi1d 320 . . 3
3 pm5.501 342 . . 3
42, 3bitr3d 258 . 2
5 nbbn 359 . . . 4
6 nbn2 346 . . . . 5
76bibi1d 320 . . . 4
85, 7syl5bbr 262 . . 3
9 nbn2 346 . . 3
108, 9bitr3d 258 . 2
114, 10pm2.61i 167 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wb 187 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 188 This theorem is referenced by:  biluk  941  xorass  1404  xorassOLD  1405  had1  1501  symdifass  3708
 Copyright terms: Public domain W3C validator