![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbir3an | GIF 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 1160 | . 2 ⊢ (𝜓 ∧ 𝜒 ∧ 𝜃) |
5 | mpbir3an.4 | . 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) | |
6 | 4, 5 | mpbir 145 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∧ w3a 963 |
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 965 |
This theorem is referenced by: limon 4437 limom 4535 issmo 6193 xpider 6508 1eluzge0 9396 2eluzge1 9398 0elunit 9799 1elunit 9800 4fvwrd4 9948 fzo0to42pr 10028 resqrexlemga 10827 sincos1sgn 11507 sincos2sgn 11508 qnnen 11980 strleun 12087 sinhalfpilem 12920 sincos4thpi 12969 sincos6thpi 12971 pigt3 12973 2logb9irr 13096 2logb9irrap 13102 |
Copyright terms: Public domain | W3C validator |