Theorem an12 642

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 639	. 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  646  an4  653  3anan12  1095  ceqsrexv  3585  rmoan  3674  2reuswap  3681  2reuswap2  3682  reuxfrd  3683  reuind  3688  2rmoswap  3696  sbccomlem  3803  indifdi  4217  elunirab  4855  axsepgfromrep  5221  opeliunxp  5654  elinxp  5929  resoprab  7392  elrnmpores  7411  ov6g  7436  opabex3d  7808  opabex3rd  7809  opabex3  7810  dfrecs3  8203  dfrecs3OLD  8204  oeeu  8434  xpassen  8853  omxpenlem  8860  dfac5lem2  9880  ltexprlem4  10795  2clim  15281  divalglem10  16111  bitsmod  16143  isssc  17532  eldmcoa  17780  issubrg  20024  isbasis2g  22098  tgval2  22106  is1stc2  22593  elflim2  23115  i1fres  24870  dvdsflsumcom  26337  vmasum  26364  logfac2  26365  axcontlem2  27333  fusgr2wsp2nb  28698  reuxfrdf  30839  1stpreima  31039  bnj849  32905  elima4  33750  elfuns  34217  dfrecs2  34252  dfrdg4  34253  bj-restuni  35268  bj-imdirco  35361  mptsnunlem  35509  relowlpssretop  35535  poimirlem27  35804  sstotbnd3  35934  an12i  36256  selconj  36258  eldmqsres  36421  inxpxrn  36521  rnxrnres  36525  refrelredund4  36748  islshpat  37031  islpln5  37549  islvol5  37593  cdleme0nex  38304  dicelval3  39194  mapdordlem1a  39648  ismnushort  41919  2reuimp  44607  elpglem3  46418