![]() |
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 1176 |
. 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 981 |
This theorem is referenced by: limon 4524 limom 4625 issmo 6302 xpider 6619 aptap 8620 1eluzge0 9587 2eluzge1 9589 0elunit 9999 1elunit 10000 fz0to3un2pr 10136 4fvwrd4 10153 fzo0to42pr 10233 resqrexlemga 11045 fprodge0 11658 fprodge1 11660 sincos1sgn 11785 sincos2sgn 11786 igz 12385 qnnen 12445 strleun 12577 cnfldstr 13683 cnsubmlem 13698 cnsubglem 13699 cnsubrglem 13700 sinhalfpilem 14452 sincos4thpi 14501 sincos6thpi 14503 pigt3 14505 2logb9irr 14629 2logb9irrap 14635 |
Copyright terms: Public domain | W3C validator |