![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbiran2 | Unicode version |
Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) (Revised by NM, 9-Jan-2015.) |
Ref | Expression |
---|---|
mpbiran2.1 |
![]() ![]() |
mpbiran2.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpbiran2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbiran2.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mpbiran2.1 |
. . 3
![]() ![]() | |
3 | 2 | biantru 286 |
. 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: reueq 2732 ss0b 3250 eusv1 4150 eusv2nf 4154 eusv2 4155 opthprc 4334 opelres 4560 f1cnvcnv 5043 fores 5058 f1orn 5079 funfvdm 5179 dfoprab2 5494 tpostpos 5820 opelreal 6726 elreal2 6728 eqresr 6733 axprecex 6764 bdeq0 9322 |
Copyright terms: Public domain | W3C validator |