![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbir3an | Unicode version |
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 9-Jan-2015.) |
Ref | Expression |
---|---|
mpbir3an.1 |
![]() ![]() |
mpbir3an.2 |
![]() ![]() |
mpbir3an.3 |
![]() ![]() |
mpbir3an.4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpbir3an |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbir3an.1 |
. . 3
![]() ![]() | |
2 | mpbir3an.2 |
. . 3
![]() ![]() | |
3 | mpbir3an.3 |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | 3pm3.2i 1177 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | mpbir3an.4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | mpbir 146 |
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 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: limon 4530 limom 4631 issmo 6313 xpider 6632 aptap 8637 1eluzge0 9604 2eluzge1 9606 0elunit 10016 1elunit 10017 fz0to3un2pr 10153 4fvwrd4 10170 fzo0to42pr 10250 resqrexlemga 11064 fprodge0 11677 fprodge1 11679 sincos1sgn 11804 sincos2sgn 11805 igz 12406 qnnen 12482 strleun 12616 cnfldstr 13866 cnsubmlem 13881 cnsubglem 13882 cnsubrglem 13883 sinhalfpilem 14672 sincos4thpi 14721 sincos6thpi 14723 pigt3 14725 2logb9irr 14849 2logb9irrap 14855 |
Copyright terms: Public domain | W3C validator |