![]() |
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.) (Proof shortened by Peter Mazsa, 18-Sep-2022.) |
Ref | Expression |
---|---|
an12 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancom 465 | . . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) | |
2 | 1 | bianass 642 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
3 | 2 | biancomi 467 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 400 |
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 210 df-an 401 |
This theorem is referenced by: an12s 649 an4 656 3anan12 1094 ceqsrexv 3565 rmoan 3650 2reuswap 3657 2reuswap2 3658 reuxfrd 3659 reuind 3664 2rmoswap 3672 sbccomlem 3772 indifdi 4184 elunirab 4807 axsepgfromrep 5160 opeliunxp 5581 elinxp 5854 resoprab 7257 elrnmpores 7276 ov6g 7301 opabex3d 7663 opabex3rd 7664 opabex3 7665 dfrecs3 8012 oeeu 8232 xpassen 8624 omxpenlem 8631 dfac5lem2 9569 ltexprlem4 10484 2clim 14962 divalglem10 15788 bitsmod 15820 isssc 17134 eldmcoa 17376 issubrg 19588 isbasis2g 21633 tgval2 21641 is1stc2 22127 elflim2 22649 i1fres 24390 dvdsflsumcom 25857 vmasum 25884 logfac2 25885 axcontlem2 26843 fusgr2wsp2nb 28203 reuxfrdf 30346 1stpreima 30548 bnj849 32410 elima4 33251 elfuns 33751 dfrecs2 33786 dfrdg4 33787 bj-restuni 34777 bj-imdirco 34870 mptsnunlem 35020 relowlpssretop 35046 poimirlem27 35349 sstotbnd3 35479 an12i 35801 selconj 35803 eldmqsres 35968 inxpxrn 36068 rnxrnres 36072 refrelredund4 36295 islshpat 36578 islpln5 37096 islvol5 37140 cdleme0nex 37851 dicelval3 38741 mapdordlem1a 39195 2reuimp 44024 elpglem3 45592 |
Copyright terms: Public domain | W3C validator |