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 1081 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | an32 642 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) | |
3 | 1, 2 | bitri 276 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: 3ancomb 1091 anandi3r 1095 rabssrabd 4055 dff1o3 6614 bropfvvvvlem 7775 tz7.49c 8071 ispos2 17546 lbsacsbs 19857 obslbs 20802 islbs4 20904 leordtvallem1 21746 trfbas2 22379 isclmp 23628 lssbn 23882 sineq0 25036 dchrelbas3 25741 nb3grpr2 27092 uspgr2wlkeq 27354 2spthd 27647 clwwlknonwwlknonb 27812 frgr2wwlkeu 28033 elicoelioo 30427 cndprobprob 31595 bnj543 32064 cusgr3cyclex 32280 elno3 33059 ellimits 33268 refsymrel2 35683 refsymrel3 35684 dfeqvrel2 35705 dfeqvrel3 35706 |
Copyright terms: Public domain | W3C validator |