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 239. Equivalent to a bi1 186like 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 6  . 2  
2  ax1 6  . 2  
3  1, 2  impbid21d 190  1 
Colors of variables: wff setvar class 
Syntax hints: wi 4 wb 184 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 ax3 8 
This theorem depends on definitions: dfbi 185 
This theorem is referenced by: 2thd 240 pm5.501 341 
Copyright terms: Public domain  W3C validator 