Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dfbi  Structured version Unicode version 
Description: Definition dfbi 178 rewritten in an abbreviated form to help intuitive understanding of that definition. Note that it is a conjunction of two implications; one which asserts properties that follow from the biconditional and one which asserts properties that imply the biconditional. (Contributed by NM, 15Aug2008.) 
Ref  Expression 

dfbi 
Step  Hyp  Ref  Expression 

1  dfbi2 610  . . 3  
2  1  biimpi 187  . 2 
3  1  biimpri 198  . 2 
4  2, 3  pm3.2i 442  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wb 177 wa 359 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 178 dfan 361 
Copyright terms: Public domain  W3C validator 