![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfbi2 | Structured version Visualization version Unicode version |
Description: A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 24-Jan-1993.) |
Ref | Expression |
---|---|
dfbi2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfbi1 195 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-an 373 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitr4i 256 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 189 df-an 373 |
This theorem is referenced by: dfbi 635 pm4.71 636 pm5.17 899 xor 902 albiim 1752 nfbid 2016 sbbi 2230 ralbiim 2922 reu8 3234 sseq2 3454 soeq2 4775 fun11 5648 dffo3 6037 isnsg2 16847 isarchi 28499 axextprim 30328 biimpexp 30348 axextndbi 30451 ifpdfbi 36117 ifpidg 36135 ifp1bi 36146 ifpbibib 36154 rp-fakeanorass 36157 frege54cor0a 36459 dffo3f 37450 aibandbiaiffaiffb 38481 aibandbiaiaiffb 38482 |
Copyright terms: Public domain | W3C validator |