![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbiran | Unicode version |
Description: Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.) (Revised by NM, 9-Jan-2015.) |
Ref | Expression |
---|---|
mpbiran.1 |
![]() ![]() |
mpbiran.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpbiran |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbiran.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mpbiran.1 |
. . 3
![]() ![]() | |
3 | 2 | biantrur 287 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | bitr4i 176 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: mpbir2an 848 unssdif 3166 unssin 3170 inssun 3171 invdif 3173 0pss 3259 pssv 3261 opabm 4008 regexmidlem1 4218 elirr 4224 en2lp 4232 peano5 4264 relop 4429 ssrnres 4706 funopab 4878 funcnv2 4902 funcnveq 4905 fnres 4958 idref 5339 rnoprab 5529 lbfzo0 8807 peano5setOLD 9400 |
Copyright terms: Public domain | W3C validator |