Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > an32 | GIF version |
Description: A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.) |
Ref | Expression |
---|---|
an32 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anass 398 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
2 | an12 550 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
3 | ancom 264 | . 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) | |
4 | 1, 2, 3 | 3bitri 205 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: an32s 557 3anan32 973 indifdir 3327 inrab2 3344 reupick 3355 unidif0 4086 resco 5038 f11o 5393 respreima 5541 dff1o6 5670 dfoprab2 5811 xpassen 6717 enq0enq 7232 elioomnf 9744 modfsummod 11220 tx1cn 12427 isms2 12612 elcncf1di 12724 |
Copyright terms: Public domain | W3C validator |