![]() |
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 1089 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | an32 644 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) | |
3 | 1, 2 | bitri 274 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 ∧ w3a 1087 |
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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: 3ancomb 1099 anandi3r 1103 rabssrabd 4040 dff1o3 6788 bropfvvvvlem 8020 tz7.49c 8389 ispos2 18201 lbsacsbs 20613 obslbs 21132 islbs4 21234 leordtvallem1 22557 trfbas2 23190 isclmp 24456 lssbn 24712 sineq0 25876 dchrelbas3 26582 elno3 26999 nb3grpr2 28229 uspgr2wlkeq 28492 2spthd 28784 clwwlknonwwlknonb 28948 frgr2wwlkeu 29169 elicoelioo 31576 cndprobprob 32929 bnj543 33396 cusgr3cyclex 33621 ellimits 34484 refsymrel2 37018 refsymrel3 37019 dfeqvrel2 37041 dfeqvrel3 37042 i0oii 46922 |
Copyright terms: Public domain | W3C validator |