Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > pm5.1im  Structured version Unicode version 
Description: Two propositions are equivalent if they are both true. Closed form of 2th 231. Equivalent to a bi1 179like 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 183  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wb 177 
This theorem is referenced by: 2thd 232 pm5.501 331 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 178 
Copyright terms: Public domain  W3C validator 