Theorem an12 632

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		anass 461	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
2		an21 631	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitr3i 269	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 198   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  an32  633  an13  634  an12s  636  an4  643  3anan12  1077  ceqsrexv  3557  rmoan  3636  2reuswap  3643  2reuswap2  3644  reuxfr3d  3645  reuind  3647  2rmoswap  3655  sbccomlem  3750  elunirab  4720  axsep  5055  opeliunxp  5465  elinxp  5732  resoprab  7084  elrnmpores  7102  ov6g  7126  opabex3d  7476  opabex3rd  7477  opabex3  7478  dfrecs3  7811  oeeu  8028  xpassen  8405  omxpenlem  8412  dfac5lem2  9342  ltexprlem4  10257  2clim  14788  divalglem10  15611  bitsmod  15643  isssc  16960  eldmcoa  17195  issubrg  19270  isbasis2g  21272  tgval2  21280  is1stc2  21766  elflim2  22288  i1fres  24021  dvdsflsumcom  25479  vmasum  25506  logfac2  25507  axcontlem2  26466  fusgr2wsp2nb  27880  1stpreima  30215  bnj849  31873  elima4  32568  elfuns  32926  dfrecs2  32961  dfrdg4  32962  bj-axsep  33652  bj-restuni  33927  mptsnunlem  34090  relowlpssretop  34116  poimirlem27  34389  sstotbnd3  34525  an12i  34849  selconj  34851  eldmqsres  35016  inxpxrn  35117  rnxrnres  35121  refrelredund4  35344  islshpat  35627  islpln5  36145  islvol5  36189  cdleme0nex  36900  dicelval3  37790  mapdordlem1a  38244  2reuimp  42745  elpglem3  44207