| 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 1096 ceqsrexv 3655 rmoan 3745 2reuswap 3752 2reuswap2 3753 reuxfrd 3754 reuind 3759 2rmoswap 3767 sbccomlemOLD 3870 indifdi 4294 elunirab 4922 axsepgfromrep 5294 opeliunxp 5752 elinxp 6037 resoprab 7551 elrnmpores 7571 ov6g 7597 opabex3d 7990 opabex3rd 7991 opabex3 7992 dfrecs3 8412 dfrecs3OLD 8413 oeeu 8641 xpassen 9106 omxpenlem 9113 dfac5lem2 10164 ltexprlem4 11079 2clim 15608 divalglem10 16439 bitsmod 16473 isssc 17864 eldmcoa 18110 issubrg 20571 isbasis2g 22955 tgval2 22963 is1stc2 23450 elflim2 23972 i1fres 25740 dvdsflsumcom 27231 vmasum 27260 logfac2 27261 axcontlem2 28980 fusgr2wsp2nb 30353 reuxfrdf 32510 1stpreima 32716 bnj849 34939 elima4 35776 elfuns 35916 dfrecs2 35951 dfrdg4 35952 bj-restuni 37098 bj-imdirco 37191 mptsnunlem 37339 relowlpssretop 37365 poimirlem27 37654 sstotbnd3 37783 an12i 38105 selconj 38107 eldmqsres 38288 inxpxrn 38396 rnxrnres 38400 refrelredund4 38636 islshpat 39018 islpln5 39537 islvol5 39581 cdleme0nex 40292 dicelval3 41182 mapdordlem1a 41636 tfsconcat0i 43358 ismnushort 44320 modelaxreplem2 44996 modelaxreplem3 44997 2reuimp 47127 elpglem3 49232 |
| Copyright terms: Public domain | W3C validator |