Theorem an12 643

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 461	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
2	1	bianass 640	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	2	biancomi 463	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  an12s  647  an4  654  3anan12  1096  ceqsrexv  3643  rmoan  3735  2reuswap  3742  2reuswap2  3743  reuxfrd  3744  reuind  3749  2rmoswap  3757  sbccomlem  3864  indifdi  4283  elunirab  4924  axsepgfromrep  5297  opeliunxp  5743  elinxp  6019  resoprab  7528  elrnmpores  7548  ov6g  7573  opabex3d  7954  opabex3rd  7955  opabex3  7956  dfrecs3  8374  dfrecs3OLD  8375  oeeu  8605  xpassen  9068  omxpenlem  9075  dfac5lem2  10121  ltexprlem4  11036  2clim  15518  divalglem10  16347  bitsmod  16379  isssc  17769  eldmcoa  18017  issubrg  20323  isbasis2g  22458  tgval2  22466  is1stc2  22953  elflim2  23475  i1fres  25230  dvdsflsumcom  26699  vmasum  26726  logfac2  26727  axcontlem2  28261  fusgr2wsp2nb  29625  reuxfrdf  31769  1stpreima  31966  bnj849  34005  elima4  34822  elfuns  34962  dfrecs2  34997  dfrdg4  34998  bj-restuni  36070  bj-imdirco  36163  mptsnunlem  36311  relowlpssretop  36337  poimirlem27  36607  sstotbnd3  36736  an12i  37058  selconj  37060  eldmqsres  37247  inxpxrn  37357  rnxrnres  37361  refrelredund4  37597  islshpat  37979  islpln5  38498  islvol5  38542  cdleme0nex  39253  dicelval3  40143  mapdordlem1a  40597  tfsconcat0i  42183  ismnushort  43148  2reuimp  45908  elpglem3  47842