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 937 unssdif 3362 unssin 3366 inssun 3367 invdif 3369 pwpwab 3960 exmidexmid 4182 opabm 4265 regexmidlem1 4517 elirr 4525 en2lp 4538 wessep 4562 peano5 4582 relop 4761 ssrnres 5053 funopab 5233 funcnv2 5258 funcnveq 5261 fnres 5314 idref 5736 rnoprab 5936 elixp 6683 djuf1olem 7030 lbfzo0 10137 txdis1cn 13072 |
Copyright terms: Public domain | W3C validator |