Theorem an12 658

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.)

Assertion

Ref	Expression
an12	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Proof of Theorem an12

Step	Hyp	Ref	Expression
1		ancom 466	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
2	1	bianass 655	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	2	biancomi 468	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an12s  662  an4  669  3anan12  1112  ceqsrexv  3617  rmoan  3705  2reuswap  3712  2reuswap2  3713  reuxfrd  3714  reuind  3719  2rmoswap  3727  sbccomlemOLD  3826  indifdi  4250  elunirab  4892  axsepgfromrep  5260  opeliunxp  5733  elinxp  6023  resoprab  7541  elrnmpores  7561  ov6g  7587  opabex3d  7971  opabex3rd  7972  opabex3  7973  dfrecs3  8368  oeeu  8598  xpassen  9069  omxpenlem  9076  dfac5lem2  10127  ltexprlem4  11042  2clim  15649  divalglem10  16485  bitsmod  16519  isssc  17902  eldmcoa  18147  issubrg  20707  isbasis2g  23142  tgval2  23150  is1stc2  23636  elflim2  24158  i1fres  25901  dvdsflsumcom  27389  vmasum  27417  logfac2  27418  axcontlem2  29352  fusgr2wsp2nb  30722  reuxfrdf  32874  1stpreima  33089  bnj849  35345  elima4  36289  elfuns  36426  dfrecs2  36463  dfrdg4  36464  bj-restuni  37780  bj-imdirco  37875  mptsnunlem  38025  relowlpssretop  38051  poimirlem27  38339  sstotbnd3  38468  an12i  38788  selconj  38790  eldmqsres  38983  inxpxrn  39108  rnxrnres  39112  refrelredund4  39409  islshpat  39832  islpln5  40350  islvol5  40394  cdleme0nex  41105  dicelval3  41995  mapdordlem1a  42449  tfsconcat0i  44113  ismnushort  45052  modelaxreplem2  45729  modelaxreplem3  45730  2reuimp  47893  elpglem3  50532