![]() |
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 300 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | bitr4i 186 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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: reueq 2887 ss0b 3407 eusv1 4381 eusv2nf 4385 eusv2 4386 opthprc 4598 opelres 4832 f1cnvcnv 5347 fores 5362 f1orn 5385 funfvdm 5492 dfoprab2 5826 tpostpos 6169 opelreal 7659 elreal2 7662 eqresr 7668 axprecex 7712 zeoxor 11602 isprm2 11834 toptopon 12224 bdeq0 13236 subctctexmid 13369 |
Copyright terms: Public domain | W3C validator |