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  3606  rmoan  3694  2reuswap  3701  2reuswap2  3702  reuxfrd  3703  reuind  3708  2rmoswap  3716  sbccomlemOLD  3817  indifdi  4243  elunirab  4875  axsepgfromrep  5236  opeliunxp  5688  elinxp  5974  resoprab  7472  elrnmpores  7492  ov6g  7518  opabex3d  7905  opabex3rd  7906  opabex3  7907  dfrecs3  8300  oeeu  8526  xpassen  8993  omxpenlem  9000  dfac5lem2  10024  ltexprlem4  10939  2clim  15483  divalglem10  16317  bitsmod  16351  isssc  17731  eldmcoa  17976  issubrg  20490  isbasis2g  22866  tgval2  22874  is1stc2  23360  elflim2  23882  i1fres  25636  dvdsflsumcom  27128  vmasum  27157  logfac2  27158  axcontlem2  28947  fusgr2wsp2nb  30318  reuxfrdf  32474  1stpreima  32694  bnj849  34960  elima4  35843  elfuns  35980  dfrecs2  36017  dfrdg4  36018  bj-restuni  37164  bj-imdirco  37257  mptsnunlem  37405  relowlpssretop  37431  poimirlem27  37710  sstotbnd3  37839  an12i  38161  selconj  38163  eldmqsres  38348  inxpxrn  38465  rnxrnres  38469  refrelredund4  38754  islshpat  39139  islpln5  39657  islvol5  39701  cdleme0nex  40412  dicelval3  41302  mapdordlem1a  41756  tfsconcat0i  43465  ismnushort  44421  modelaxreplem2  45099  modelaxreplem3  45100  2reuimp  47242  elpglem3  49841