Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > pm5.1im  Structured version Unicode version 
Description: Two propositions are equivalent if they are both true. Closed form of 2th 163. Equivalent to a bi1 111like 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 119  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wb 98 
This theorem was proved from axioms: ax1 5 ax2 6 axmp 7 axia2 100 axia3 101 
This theorem depends on definitions: dfbi 110 
This theorem is referenced by: 2thd 164 pm5.501 233 
Copyright terms: Public domain  W3C validator 