![]() |
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 1177 | . 2 ⊢ (𝜓 ∧ 𝜒 ∧ 𝜃) |
5 | mpbir3an.4 | . 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) | |
6 | 4, 5 | mpbir 146 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ∧ w3a 980 |
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 982 |
This theorem is referenced by: limon 4530 limom 4631 issmo 6314 xpider 6633 aptap 8638 1eluzge0 9606 2eluzge1 9608 0elunit 10018 1elunit 10019 fz0to3un2pr 10155 4fvwrd4 10172 fzo0to42pr 10252 resqrexlemga 11067 fprodge0 11680 fprodge1 11682 sincos1sgn 11807 sincos2sgn 11808 igz 12409 qnnen 12485 strleun 12619 cnfldstr 13883 cnsubmlem 13898 cnsubglem 13899 cnsubrglem 13900 sinhalfpilem 14689 sincos4thpi 14738 sincos6thpi 14740 pigt3 14742 2logb9irr 14866 2logb9irrap 14872 |
Copyright terms: Public domain | W3C validator |