New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 437 | . . 3 ⊢ ((φ ∧ ψ) ↔ (ψ ∧ φ)) | |
2 | 1 | anbi1i 676 | . 2 ⊢ (((φ ∧ ψ) ∧ χ) ↔ ((ψ ∧ φ) ∧ χ)) |
3 | anass 630 | . 2 ⊢ (((φ ∧ ψ) ∧ χ) ↔ (φ ∧ (ψ ∧ χ))) | |
4 | anass 630 | . 2 ⊢ (((ψ ∧ φ) ∧ χ) ↔ (ψ ∧ (φ ∧ χ))) | |
5 | 2, 3, 4 | 3bitr3i 266 | 1 ⊢ ((φ ∧ (ψ ∧ χ)) ↔ (ψ ∧ (φ ∧ χ))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 ∧ wa 358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 df-an 360 |
This theorem is referenced by: an32 773 an13 774 an12s 776 an4 797 ceqsrexv 2973 rmoan 3035 2reuswap 3039 reuind 3040 sbccomlem 3117 elunirab 3905 pw1in 4165 eluni1g 4173 insklem 4305 addcass 4416 setconslem4 4735 opeliunxp 4821 elres 4996 dff1o2 5292 dfoprab2 5559 resoprab 5582 ov6g 5601 nmembers1lem1 6269 |
Copyright terms: Public domain | W3C validator |