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  1096  ceqsrexv  3655  rmoan  3745  2reuswap  3752  2reuswap2  3753  reuxfrd  3754  reuind  3759  2rmoswap  3767  sbccomlemOLD  3870  indifdi  4294  elunirab  4922  axsepgfromrep  5294  opeliunxp  5752  elinxp  6037  resoprab  7551  elrnmpores  7571  ov6g  7597  opabex3d  7990  opabex3rd  7991  opabex3  7992  dfrecs3  8412  dfrecs3OLD  8413  oeeu  8641  xpassen  9106  omxpenlem  9113  dfac5lem2  10164  ltexprlem4  11079  2clim  15608  divalglem10  16439  bitsmod  16473  isssc  17864  eldmcoa  18110  issubrg  20571  isbasis2g  22955  tgval2  22963  is1stc2  23450  elflim2  23972  i1fres  25740  dvdsflsumcom  27231  vmasum  27260  logfac2  27261  axcontlem2  28980  fusgr2wsp2nb  30353  reuxfrdf  32510  1stpreima  32716  bnj849  34939  elima4  35776  elfuns  35916  dfrecs2  35951  dfrdg4  35952  bj-restuni  37098  bj-imdirco  37191  mptsnunlem  37339  relowlpssretop  37365  poimirlem27  37654  sstotbnd3  37783  an12i  38105  selconj  38107  eldmqsres  38288  inxpxrn  38396  rnxrnres  38400  refrelredund4  38636  islshpat  39018  islpln5  39537  islvol5  39581  cdleme0nex  40292  dicelval3  41182  mapdordlem1a  41636  tfsconcat0i  43358  ismnushort  44320  modelaxreplem2  44996  modelaxreplem3  44997  2reuimp  47127  elpglem3  49232