Theorem an12 655

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 464	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
2	1	bianass 652	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	2	biancomi 466	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  an12s  659  an4  666  3anan12  1106  ceqsrexv  3613  rmoan  3700  2reuswap  3707  2reuswap2  3708  reuxfrd  3709  reuind  3714  2rmoswap  3722  sbccomlemOLD  3821  indifdi  4244  elunirab  4877  axsepgfromrep  5241  opeliunxp  5710  elinxp  6001  resoprab  7508  elrnmpores  7528  ov6g  7554  opabex3d  7940  opabex3rd  7941  opabex3  7942  dfrecs3  8336  oeeu  8566  xpassen  9036  omxpenlem  9043  dfac5lem2  10073  ltexprlem4  10990  2clim  15589  divalglem10  16426  bitsmod  16460  isssc  17843  eldmcoa  18088  issubrg  20607  isbasis2g  22995  tgval2  23003  is1stc2  23489  elflim2  24011  i1fres  25754  dvdsflsumcom  27239  vmasum  27267  logfac2  27268  axcontlem2  29122  fusgr2wsp2nb  30492  reuxfrdf  32648  1stpreima  32869  bnj849  35180  elima4  36086  elfuns  36223  dfrecs2  36260  dfrdg4  36261  bj-restuni  37547  bj-imdirco  37642  mptsnunlem  37792  relowlpssretop  37818  poimirlem27  38106  sstotbnd3  38235  an12i  38557  selconj  38559  eldmqsres  38752  inxpxrn  38877  rnxrnres  38881  refrelredund4  39178  islshpat  39601  islpln5  40119  islvol5  40163  cdleme0nex  40874  dicelval3  41764  mapdordlem1a  42218  tfsconcat0i  43882  ismnushort  44837  modelaxreplem2  45515  modelaxreplem3  45516  2reuimp  47669  elpglem3  50294