|   | 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 1088 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
| 2 | an32 646 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) | |
| 3 | 1, 2 | bitri 275 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ wa 395 ∧ w3a 1086 | 
| 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 207 df-an 396 df-3an 1088 | 
| This theorem is referenced by: 3ancomb 1098 anandi3r 1102 rabssrabd 4082 dff1o3 6853 bropfvvvvlem 8117 tz7.49c 8487 ispos2 18362 lbsacsbs 21159 obslbs 21751 islbs4 21853 leordtvallem1 23219 trfbas2 23852 isclmp 25131 lssbn 25387 sineq0 26567 dchrelbas3 27283 elno3 27701 nb3grpr2 29401 uspgr2wlkeq 29665 2spthd 29962 clwwlknonwwlknonb 30126 frgr2wwlkeu 30347 elicoelioo 32781 cndprobprob 34441 bnj543 34908 cusgr3cyclex 35142 ellimits 35912 refsymrel2 38569 refsymrel3 38570 dfeqvrel2 38592 dfeqvrel3 38593 i0oii 48824 | 
| Copyright terms: Public domain | W3C validator |