Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > pm5.7  Unicode version 
Description: Disjunction distributes over the biconditional. Theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbidi 903. (Contributed by Roy F. Longton, 21Jun2005.) 
Ref  Expression 

pm5.7 
Step  Hyp  Ref  Expression 

1  orbidi 903  . 2  
2  orcom 378  . . 3  
3  orcom 378  . . 3  
4  2, 3  bibi12i 308  . 2 
5  1, 4  bitr2i 243  1 
Colors of variables: wff set class 
Syntax hints: wb 178 wo 359 
This theorem was proved from axioms: ax1 7 ax2 8 ax3 9 axmp 10 
This theorem depends on definitions: dfbi 179 dfor 361 
Copyright terms: Public domain  W3C validator 