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 1159 | . 2 |
5 | mpbir3an.4 | . 2 | |
6 | 4, 5 | mpbir 145 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 w3a 962 |
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 964 |
This theorem is referenced by: limon 4429 limom 4527 issmo 6185 xpider 6500 1eluzge0 9369 2eluzge1 9371 0elunit 9769 1elunit 9770 4fvwrd4 9917 fzo0to42pr 9997 resqrexlemga 10795 sincos1sgn 11471 sincos2sgn 11472 qnnen 11944 strleun 12048 sinhalfpilem 12872 sincos4thpi 12921 sincos6thpi 12923 pigt3 12925 |
Copyright terms: Public domain | W3C validator |