Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > biass  Unicode version 
Description: Associative law for the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs", Annals of Pure and Applied Logic, 113:207224, 2002, http://www.cs.utexas.edu/users/ailab/pubview.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, 8Jan2005.) (Proof shortened by Juha Arpiainen, 19Jan2006.) (Proof shortened by Wolf Lammen, 21Sep2013.) 
Ref  Expression 

biass 
Step  Hyp  Ref  Expression 

1  pm5.501 330  . . . 4  
2  1  bibi1d 310  . . 3 
3  pm5.501 330  . . 3  
4  2, 3  bitr3d 246  . 2 
5  nbbn 347  . . . 4  
6  nbn2 334  . . . . 5  
7  6  bibi1d 310  . . . 4 
8  5, 7  syl5bbr 250  . . 3 
9  nbn2 334  . . 3  
10  8, 9  bitr3d 246  . 2 
11  4, 10  pm2.61i 156  1 
Colors of variables: wff set class 
Syntax hints: wn 3 wb 176 
This theorem is referenced by: biluk 899 xorass 1299 had1 1392 symdifass 24371 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 177 
Copyright terms: Public domain  W3C validator 