Theorem an12 644

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 641	. 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  648  an4  655  3anan12  1096  ceqsrexv  3668  rmoan  3761  2reuswap  3768  2reuswap2  3769  reuxfrd  3770  reuind  3775  2rmoswap  3783  sbccomlemOLD  3892  indifdi  4313  elunirab  4946  axsepgfromrep  5315  opeliunxp  5767  elinxp  6048  resoprab  7568  elrnmpores  7588  ov6g  7614  opabex3d  8006  opabex3rd  8007  opabex3  8008  dfrecs3  8428  dfrecs3OLD  8429  oeeu  8659  xpassen  9132  omxpenlem  9139  dfac5lem2  10193  ltexprlem4  11108  2clim  15618  divalglem10  16450  bitsmod  16482  isssc  17881  eldmcoa  18132  issubrg  20599  isbasis2g  22976  tgval2  22984  is1stc2  23471  elflim2  23993  i1fres  25760  dvdsflsumcom  27249  vmasum  27278  logfac2  27279  axcontlem2  28998  fusgr2wsp2nb  30366  reuxfrdf  32519  1stpreima  32718  bnj849  34901  elima4  35739  elfuns  35879  dfrecs2  35914  dfrdg4  35915  bj-restuni  37063  bj-imdirco  37156  mptsnunlem  37304  relowlpssretop  37330  poimirlem27  37607  sstotbnd3  37736  an12i  38058  selconj  38060  eldmqsres  38243  inxpxrn  38351  rnxrnres  38355  refrelredund4  38591  islshpat  38973  islpln5  39492  islvol5  39536  cdleme0nex  40247  dicelval3  41137  mapdordlem1a  41591  tfsconcat0i  43307  ismnushort  44270  2reuimp  47030  elpglem3  48805