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 727 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜓 ∧ 𝜑) ∧ 𝜒)) |
3 | anass 679 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
4 | anass 679 | . 2 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
5 | 2, 3, 4 | 3bitr3i 289 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ 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 196 df-an 385 |
This theorem is referenced by: an32 835 an13 836 an12s 839 an4 861 ceqsrexv 3306 rmoan 3373 2reuswap 3377 reuind 3378 sbccomlem 3475 elunirab 4384 axsep 4708 reuxfr2d 4817 opeliunxp 5093 elres 5355 resoprab 6654 elrnmpt2res 6672 ov6g 6696 opabex3d 7037 opabex3 7038 dfrecs3 7356 oeeu 7570 xpassen 7939 omxpenlem 7946 dfac5lem2 8830 ltexprlem4 9740 rexuz2 11615 2clim 14151 divalglem10 14963 bitsmod 14996 isssc 16303 eldmcoa 16538 issubrg 18603 isbasis2g 20563 tgval2 20571 is1stc2 21055 elflim2 21578 i1fres 23278 dvdsflsumcom 24714 vmasum 24741 logfac2 24742 axcontlem2 25645 2reuswap2 28712 reuxfr3d 28713 1stpreima 28867 bnj849 30249 elima4 30924 nofulllem5 31105 elfuns 31192 brimg 31214 dfrecs2 31227 dfrdg4 31228 bj-axsep 31981 bj-restuni 32231 mptsnunlem 32361 relowlpssretop 32388 poimirlem27 32606 sstotbnd3 32745 an12i 33070 selconj 33072 islshpat 33322 islpln5 33839 islvol5 33883 cdleme0nex 34595 dicelval3 35487 mapdordlem1a 35941 2rmoswap 39833 elpglem3 42255 |
Copyright terms: Public domain | W3C validator |