![]() |
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 2891 rmoan 2961 2reuswapdc 2965 reuind 2966 2rmorex 2967 sbccomlem 3061 elunirab 3849 rexxfrd 4495 opeliunxp 4715 elres 4979 resoprab 6015 ov6g 6058 opabex3d 6175 opabex3 6176 xpassen 6886 distrnqg 7449 distrnq0 7521 rexuz2 9649 2clim 11447 issubrg 13720 isbasis2g 14224 tgval2 14230 |
Copyright terms: Public domain | W3C validator |