Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > pm5.1im  Unicode version 
Description: Two propositions are equivalent if they are both true. Closed form of 2th 230. Equivalent to a bi1 178like version of the xorconnective. This theorem stays true, no matter how you permute its operands. This is evident from its sharper version . (Contributed by Wolf Lammen, 12May2013.) 
Ref  Expression 

pm5.1im 
Step  Hyp  Ref  Expression 

1  ax1 5  . 2  
2  ax1 5  . 2  
3  1, 2  impbid21d 182  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wb 176 
This theorem is referenced by: 2thd 231 pm5.501 330 
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 