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  3597  rmoan  3685  2reuswap  3692  2reuswap2  3693  reuxfrd  3694  reuind  3699  2rmoswap  3707  sbccomlemOLD  3808  indifdi  4234  elunirab  4865  axsepgfromrep  5229  opeliunxp  5698  elinxp  5984  resoprab  7485  elrnmpores  7505  ov6g  7531  opabex3d  7918  opabex3rd  7919  opabex3  7920  dfrecs3  8312  oeeu  8539  xpassen  9009  omxpenlem  9016  dfac5lem2  10046  ltexprlem4  10962  2clim  15534  divalglem10  16371  bitsmod  16405  isssc  17787  eldmcoa  18032  issubrg  20548  isbasis2g  22913  tgval2  22921  is1stc2  23407  elflim2  23929  i1fres  25672  dvdsflsumcom  27151  vmasum  27179  logfac2  27180  axcontlem2  29034  fusgr2wsp2nb  30404  reuxfrdf  32560  1stpreima  32780  bnj849  35067  elima4  35958  elfuns  36095  dfrecs2  36132  dfrdg4  36133  bj-restuni  37409  bj-imdirco  37504  mptsnunlem  37654  relowlpssretop  37680  poimirlem27  37968  sstotbnd3  38097  an12i  38419  selconj  38421  eldmqsres  38614  inxpxrn  38739  rnxrnres  38743  refrelredund4  39040  islshpat  39463  islpln5  39981  islvol5  40025  cdleme0nex  40736  dicelval3  41626  mapdordlem1a  42080  tfsconcat0i  43773  ismnushort  44728  modelaxreplem2  45406  modelaxreplem3  45407  2reuimp  47563  elpglem3  50188