Theorem an12 645

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 642	. 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  649  an4  656  3anan12  1095  ceqsrexv  3609  rmoan  3697  2reuswap  3704  2reuswap2  3705  reuxfrd  3706  reuind  3711  2rmoswap  3719  sbccomlemOLD  3820  indifdi  4246  elunirab  4878  axsepgfromrep  5239  opeliunxp  5691  elinxp  5978  resoprab  7476  elrnmpores  7496  ov6g  7522  opabex3d  7909  opabex3rd  7910  opabex3  7911  dfrecs3  8304  oeeu  8531  xpassen  8999  omxpenlem  9006  dfac5lem2  10034  ltexprlem4  10950  2clim  15495  divalglem10  16329  bitsmod  16363  isssc  17744  eldmcoa  17989  issubrg  20504  isbasis2g  22892  tgval2  22900  is1stc2  23386  elflim2  23908  i1fres  25662  dvdsflsumcom  27154  vmasum  27183  logfac2  27184  axcontlem2  29038  fusgr2wsp2nb  30409  reuxfrdf  32565  1stpreima  32786  bnj849  35081  elima4  35970  elfuns  36107  dfrecs2  36144  dfrdg4  36145  bj-restuni  37302  bj-imdirco  37395  mptsnunlem  37543  relowlpssretop  37569  poimirlem27  37848  sstotbnd3  37977  an12i  38299  selconj  38301  eldmqsres  38486  inxpxrn  38603  rnxrnres  38607  refrelredund4  38892  islshpat  39277  islpln5  39795  islvol5  39839  cdleme0nex  40550  dicelval3  41440  mapdordlem1a  41894  tfsconcat0i  43587  ismnushort  44542  modelaxreplem2  45220  modelaxreplem3  45221  2reuimp  47361  elpglem3  49958