| 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 460 | . . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) | |
| 2 | 1 | bianass 642 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
| 3 | 2 | biancomi 462 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 |
| 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 |
| This theorem is referenced by: an12s 649 an4 656 3anan12 1095 ceqsrexv 3606 rmoan 3694 2reuswap 3701 2reuswap2 3702 reuxfrd 3703 reuind 3708 2rmoswap 3716 sbccomlemOLD 3817 indifdi 4243 elunirab 4873 axsepgfromrep 5234 opeliunxp 5686 elinxp 5972 resoprab 7470 elrnmpores 7490 ov6g 7516 opabex3d 7903 opabex3rd 7904 opabex3 7905 dfrecs3 8298 oeeu 8524 xpassen 8991 omxpenlem 8998 dfac5lem2 10022 ltexprlem4 10937 2clim 15481 divalglem10 16315 bitsmod 16349 isssc 17729 eldmcoa 17974 issubrg 20488 isbasis2g 22864 tgval2 22872 is1stc2 23358 elflim2 23880 i1fres 25634 dvdsflsumcom 27126 vmasum 27155 logfac2 27156 axcontlem2 28945 fusgr2wsp2nb 30316 reuxfrdf 32472 1stpreima 32692 bnj849 34958 elima4 35841 elfuns 35978 dfrecs2 36015 dfrdg4 36016 bj-restuni 37162 bj-imdirco 37255 mptsnunlem 37403 relowlpssretop 37429 poimirlem27 37707 sstotbnd3 37836 an12i 38158 selconj 38160 eldmqsres 38345 inxpxrn 38462 rnxrnres 38466 refrelredund4 38751 islshpat 39136 islpln5 39654 islvol5 39698 cdleme0nex 40409 dicelval3 41299 mapdordlem1a 41753 tfsconcat0i 43462 ismnushort 44418 modelaxreplem2 45096 modelaxreplem3 45097 2reuimp 47239 elpglem3 49838 |
| Copyright terms: Public domain | W3C validator |