![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > an12 | Structured version Visualization version GIF version |
Description: Swap two conjuncts. Note that the first digit (1) in the label refers to the outer conjunct position, and the next digit (2) to the inner conjunct position. (Contributed by NM, 12-Mar-1995.) |
Ref | Expression |
---|---|
an12 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancom 465 | . . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) | |
2 | 1 | anbi1i 733 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜓 ∧ 𝜑) ∧ 𝜒)) |
3 | anass 684 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
4 | anass 684 | . 2 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
5 | 2, 3, 4 | 3bitr3i 290 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 |
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 385 |
This theorem is referenced by: an32 874 an13 875 an12s 878 an4 900 3anan12 1082 ceqsrexv 3475 rmoan 3547 2reuswap 3551 reuind 3552 sbccomlem 3649 elunirab 4600 axsep 4932 reuxfr2d 5040 opeliunxp 5327 elres 5593 resoprab 6922 elrnmpt2res 6940 ov6g 6964 opabex3d 7311 opabex3 7312 dfrecs3 7639 oeeu 7854 xpassen 8221 omxpenlem 8228 dfac5lem2 9157 ltexprlem4 10073 rexuz2 11952 2clim 14522 divalglem10 15347 bitsmod 15380 isssc 16701 eldmcoa 16936 issubrg 19002 isbasis2g 20974 tgval2 20982 is1stc2 21467 elflim2 21989 i1fres 23691 dvdsflsumcom 25134 vmasum 25161 logfac2 25162 axcontlem2 26065 fusgr2wsp2nb 27509 2reuswap2 29657 reuxfr3d 29658 1stpreima 29814 bnj849 31323 elima4 32005 elfuns 32349 brimg 32371 dfrecs2 32384 dfrdg4 32385 bj-axsep 33121 bj-restuni 33374 mptsnunlem 33514 relowlpssretop 33541 poimirlem27 33767 sstotbnd3 33906 an12i 34231 selconj 34233 eldmqsres 34393 inxpxrn 34494 rnxrnres 34498 islshpat 34825 islpln5 35342 islvol5 35386 cdleme0nex 36098 dicelval3 36989 mapdordlem1a 37443 2rmoswap 41708 elpglem3 42987 |
Copyright terms: Public domain | W3C validator |