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 301 | . 2 |
4 | 1, 3 | bitr4i 186 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpbir2an 927 unssdif 3342 unssin 3346 inssun 3347 invdif 3349 pwpwab 3936 exmidexmid 4157 opabm 4240 regexmidlem1 4492 elirr 4500 en2lp 4513 wessep 4537 peano5 4557 relop 4736 ssrnres 5028 funopab 5205 funcnv2 5230 funcnveq 5233 fnres 5286 idref 5707 rnoprab 5904 elixp 6650 djuf1olem 6997 lbfzo0 10080 txdis1cn 12678 |
Copyright terms: Public domain | W3C validator |