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 1170 | . 2 |
5 | mpbir3an.4 | . 2 | |
6 | 4, 5 | mpbir 145 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 w3a 973 |
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 df-3an 975 |
This theorem is referenced by: limon 4495 limom 4596 issmo 6265 xpider 6582 1eluzge0 9526 2eluzge1 9528 0elunit 9936 1elunit 9937 fz0to3un2pr 10072 4fvwrd4 10089 fzo0to42pr 10169 resqrexlemga 10980 fprodge0 11593 fprodge1 11595 sincos1sgn 11720 sincos2sgn 11721 igz 12319 qnnen 12379 strleun 12500 sinhalfpilem 13471 sincos4thpi 13520 sincos6thpi 13522 pigt3 13524 2logb9irr 13648 2logb9irrap 13654 |
Copyright terms: Public domain | W3C validator |