![]() |
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 253 | . . 3 ⊢ ((φ ∧ ψ) ↔ (ψ ∧ φ)) | |
2 | 1 | anbi1i 431 | . 2 ⊢ (((φ ∧ ψ) ∧ χ) ↔ ((ψ ∧ φ) ∧ χ)) |
3 | anass 381 | . 2 ⊢ (((φ ∧ ψ) ∧ χ) ↔ (φ ∧ (ψ ∧ χ))) | |
4 | anass 381 | . 2 ⊢ (((ψ ∧ φ) ∧ χ) ↔ (ψ ∧ (φ ∧ χ))) | |
5 | 2, 3, 4 | 3bitr3i 199 | 1 ⊢ ((φ ∧ (ψ ∧ χ)) ↔ (ψ ∧ (φ ∧ χ))) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 97 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: an32 496 an13 497 an12s 499 an4 520 ceqsrexv 2668 rmoan 2733 2reuswapdc 2737 reuind 2738 2rmorex 2739 sbccomlem 2826 elunirab 3584 rexxfrd 4161 opeliunxp 4338 elres 4589 resoprab 5539 ov6g 5580 opabex3d 5690 opabex3 5691 xpassen 6240 distrnqg 6371 distrnq0 6442 rexuz2 8300 |
Copyright terms: Public domain | W3C validator |