![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > an12 | GIF version |
Description: Swap two conjuncts. Note that the first digit (1) in the label refers to the outer conjunct position, and the next digit (2) to the inner conjunct position. (Contributed by NM, 12-Mar-1995.) |
Ref | Expression |
---|---|
an12 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancom 266 | . . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) | |
2 | 1 | anbi1i 458 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜓 ∧ 𝜑) ∧ 𝜒)) |
3 | anass 401 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
4 | anass 401 | . 2 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
5 | 2, 3, 4 | 3bitr3i 210 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 ↔ wb 105 |
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 |
This theorem is referenced by: an32 562 an13 563 an12s 565 an4 586 ceqsrexv 2867 rmoan 2937 2reuswapdc 2941 reuind 2942 2rmorex 2943 sbccomlem 3037 elunirab 3822 rexxfrd 4463 opeliunxp 4681 elres 4943 resoprab 5970 ov6g 6011 opabex3d 6121 opabex3 6122 xpassen 6829 distrnqg 7385 distrnq0 7457 rexuz2 9579 2clim 11304 issubrg 13342 isbasis2g 13476 tgval2 13482 |
Copyright terms: Public domain | W3C validator |