![]() |
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 462 | . . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) | |
2 | 1 | bianass 641 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
3 | 2 | biancomi 464 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: an12s 648 an4 655 3anan12 1097 ceqsrexv 3641 rmoan 3733 2reuswap 3740 2reuswap2 3741 reuxfrd 3742 reuind 3747 2rmoswap 3755 sbccomlem 3862 indifdi 4281 elunirab 4920 axsepgfromrep 5293 opeliunxp 5738 elinxp 6014 resoprab 7513 elrnmpores 7533 ov6g 7558 opabex3d 7939 opabex3rd 7940 opabex3 7941 dfrecs3 8359 dfrecs3OLD 8360 oeeu 8591 xpassen 9054 omxpenlem 9061 dfac5lem2 10106 ltexprlem4 11021 2clim 15503 divalglem10 16332 bitsmod 16364 isssc 17754 eldmcoa 18002 issubrg 20340 isbasis2g 22420 tgval2 22428 is1stc2 22915 elflim2 23437 i1fres 25192 dvdsflsumcom 26659 vmasum 26686 logfac2 26687 axcontlem2 28190 fusgr2wsp2nb 29554 reuxfrdf 31696 1stpreima 31899 bnj849 33867 elima4 34678 elfuns 34818 dfrecs2 34853 dfrdg4 34854 bj-restuni 35883 bj-imdirco 35976 mptsnunlem 36124 relowlpssretop 36150 poimirlem27 36420 sstotbnd3 36550 an12i 36872 selconj 36874 eldmqsres 37061 inxpxrn 37171 rnxrnres 37175 refrelredund4 37411 islshpat 37793 islpln5 38312 islvol5 38356 cdleme0nex 39067 dicelval3 39957 mapdordlem1a 40411 tfsconcat0i 41966 ismnushort 42931 2reuimp 45696 elpglem3 47598 |
Copyright terms: Public domain | W3C validator |