Theorem an12 646

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 460	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
2	1	bianass 643	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	2	biancomi 462	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  an12s  650  an4  657  3anan12  1096  ceqsrexv  3611  rmoan  3699  2reuswap  3706  2reuswap2  3707  reuxfrd  3708  reuind  3713  2rmoswap  3721  sbccomlemOLD  3822  indifdi  4248  elunirab  4880  axsepgfromrep  5241  opeliunxp  5699  elinxp  5986  resoprab  7486  elrnmpores  7506  ov6g  7532  opabex3d  7919  opabex3rd  7920  opabex3  7921  dfrecs3  8314  oeeu  8541  xpassen  9011  omxpenlem  9018  dfac5lem2  10046  ltexprlem4  10962  2clim  15507  divalglem10  16341  bitsmod  16375  isssc  17756  eldmcoa  18001  issubrg  20516  isbasis2g  22904  tgval2  22912  is1stc2  23398  elflim2  23920  i1fres  25674  dvdsflsumcom  27166  vmasum  27195  logfac2  27196  axcontlem2  29050  fusgr2wsp2nb  30421  reuxfrdf  32576  1stpreima  32796  bnj849  35100  elima4  35989  elfuns  36126  dfrecs2  36163  dfrdg4  36164  bj-restuni  37347  bj-imdirco  37442  mptsnunlem  37590  relowlpssretop  37616  poimirlem27  37895  sstotbnd3  38024  an12i  38346  selconj  38348  eldmqsres  38541  inxpxrn  38666  rnxrnres  38670  refrelredund4  38967  islshpat  39390  islpln5  39908  islvol5  39952  cdleme0nex  40663  dicelval3  41553  mapdordlem1a  42007  tfsconcat0i  43699  ismnushort  44654  modelaxreplem2  45332  modelaxreplem3  45333  2reuimp  47472  elpglem3  50069