![]() |
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 1175 | . 2 ⊢ (𝜓 ∧ 𝜒 ∧ 𝜃) |
5 | mpbir3an.4 | . 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) | |
6 | 4, 5 | mpbir 146 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ∧ w3a 978 |
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 980 |
This theorem is referenced by: limon 4508 limom 4609 issmo 6282 xpider 6599 1eluzge0 9550 2eluzge1 9552 0elunit 9960 1elunit 9961 fz0to3un2pr 10096 4fvwrd4 10113 fzo0to42pr 10193 resqrexlemga 11003 fprodge0 11616 fprodge1 11618 sincos1sgn 11743 sincos2sgn 11744 igz 12342 qnnen 12402 strleun 12532 sinhalfpilem 13845 sincos4thpi 13894 sincos6thpi 13896 pigt3 13898 2logb9irr 14022 2logb9irrap 14028 |
Copyright terms: Public domain | W3C validator |