Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3anan32 | Structured version Visualization version GIF version |
Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
3anan32 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 1039 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | an32 839 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) | |
3 | 1, 2 | bitri 264 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 384 ∧ w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: anandi3r 1053 dff1o3 6143 bropfvvvvlem 7256 tz7.49c 7541 ispos2 16948 lbsacsbs 19156 obslbs 20074 islbs4 20171 leordtvallem1 21014 trfbas2 21647 isclmp 22897 lssbn 23148 sineq0 24273 dchrelbas3 24963 nb3grpr2 26285 uspgr2wlkeq 26542 2spthd 26837 frgr2wwlkeu 27191 elicoelioo 29540 cndprobprob 30500 bnj543 30963 elno3 31808 ellimits 32017 |
Copyright terms: Public domain | W3C validator |