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  3634  rmoan  3722  2reuswap  3729  2reuswap2  3730  reuxfrd  3731  reuind  3736  2rmoswap  3744  sbccomlemOLD  3845  indifdi  4269  elunirab  4898  axsepgfromrep  5264  opeliunxp  5721  elinxp  6006  resoprab  7523  elrnmpores  7543  ov6g  7569  opabex3d  7962  opabex3rd  7963  opabex3  7964  dfrecs3  8384  dfrecs3OLD  8385  oeeu  8613  xpassen  9078  omxpenlem  9085  dfac5lem2  10136  ltexprlem4  11051  2clim  15586  divalglem10  16419  bitsmod  16453  isssc  17831  eldmcoa  18076  issubrg  20529  isbasis2g  22884  tgval2  22892  is1stc2  23378  elflim2  23900  i1fres  25656  dvdsflsumcom  27148  vmasum  27177  logfac2  27178  axcontlem2  28890  fusgr2wsp2nb  30261  reuxfrdf  32418  1stpreima  32630  bnj849  34902  elima4  35739  elfuns  35879  dfrecs2  35914  dfrdg4  35915  bj-restuni  37061  bj-imdirco  37154  mptsnunlem  37302  relowlpssretop  37328  poimirlem27  37617  sstotbnd3  37746  an12i  38068  selconj  38070  eldmqsres  38251  inxpxrn  38359  rnxrnres  38363  refrelredund4  38599  islshpat  38981  islpln5  39500  islvol5  39544  cdleme0nex  40255  dicelval3  41145  mapdordlem1a  41599  tfsconcat0i  43316  ismnushort  44273  modelaxreplem2  44952  modelaxreplem3  44953  2reuimp  47092  elpglem3  49525