Theorem an12 657

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 465	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
2	1	bianass 654	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	2	biancomi 467	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  an12s  661  an4  668  3anan12  1110  ceqsrexv  3617  rmoan  3705  2reuswap  3712  2reuswap2  3713  reuxfrd  3714  reuind  3719  2rmoswap  3727  sbccomlemOLD  3826  indifdi  4249  elunirab  4883  axsepgfromrep  5249  opeliunxp  5719  elinxp  6009  resoprab  7518  elrnmpores  7538  ov6g  7564  opabex3d  7950  opabex3rd  7951  opabex3  7952  dfrecs3  8347  oeeu  8577  xpassen  9047  omxpenlem  9054  dfac5lem2  10096  ltexprlem4  11012  2clim  15613  divalglem10  16450  bitsmod  16484  isssc  17867  eldmcoa  18112  issubrg  20647  isbasis2g  23066  tgval2  23074  is1stc2  23560  elflim2  24082  i1fres  25825  dvdsflsumcom  27310  vmasum  27338  logfac2  27339  axcontlem2  29224  fusgr2wsp2nb  30594  reuxfrdf  32747  1stpreima  32964  bnj849  35230  elima4  36139  elfuns  36276  dfrecs2  36313  dfrdg4  36314  bj-restuni  37599  bj-imdirco  37694  mptsnunlem  37844  relowlpssretop  37870  poimirlem27  38158  sstotbnd3  38287  an12i  38609  selconj  38611  eldmqsres  38804  inxpxrn  38929  rnxrnres  38933  refrelredund4  39230  islshpat  39653  islpln5  40171  islvol5  40215  cdleme0nex  40926  dicelval3  41816  mapdordlem1a  42270  tfsconcat0i  43934  ismnushort  44875  modelaxreplem2  45553  modelaxreplem3  45554  2reuimp  47707  elpglem3  50342