![]() |
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 4527 limom 4628 issmo 6307 xpider 6624 aptap 8626 1eluzge0 9593 2eluzge1 9595 0elunit 10005 1elunit 10006 fz0to3un2pr 10142 4fvwrd4 10159 fzo0to42pr 10239 resqrexlemga 11051 fprodge0 11664 fprodge1 11666 sincos1sgn 11791 sincos2sgn 11792 igz 12391 qnnen 12456 strleun 12588 cnfldstr 13833 cnsubmlem 13848 cnsubglem 13849 cnsubrglem 13850 sinhalfpilem 14615 sincos4thpi 14664 sincos6thpi 14666 pigt3 14668 2logb9irr 14792 2logb9irrap 14798 |
Copyright terms: Public domain | W3C validator |