Theorem an12 657

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 465	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
2	1	bianass 654	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	2	biancomi 467	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  an12s  661  an4  668  3anan12  1112  ceqsrexv  3615  rmoan  3703  2reuswap  3710  2reuswap2  3711  reuxfrd  3712  reuind  3717  2rmoswap  3725  sbccomlemOLD  3824  indifdi  4248  elunirab  4888  axsepgfromrep  5256  opeliunxp  5730  elinxp  6020  resoprab  7530  elrnmpores  7550  ov6g  7576  opabex3d  7963  opabex3rd  7964  opabex3  7965  dfrecs3  8360  oeeu  8590  xpassen  9060  omxpenlem  9067  dfac5lem2  10109  ltexprlem4  11025  2clim  15625  divalglem10  16461  bitsmod  16495  isssc  17878  eldmcoa  18123  issubrg  20657  isbasis2g  23086  tgval2  23094  is1stc2  23580  elflim2  24102  i1fres  25845  dvdsflsumcom  27333  vmasum  27361  logfac2  27362  axcontlem2  29296  fusgr2wsp2nb  30666  reuxfrdf  32818  1stpreima  33033  bnj849  35294  elima4  36249  elfuns  36386  dfrecs2  36423  dfrdg4  36424  bj-restuni  37720  bj-imdirco  37815  mptsnunlem  37965  relowlpssretop  37991  poimirlem27  38279  sstotbnd3  38408  an12i  38728  selconj  38730  eldmqsres  38923  inxpxrn  39048  rnxrnres  39052  refrelredund4  39349  islshpat  39772  islpln5  40290  islvol5  40334  cdleme0nex  41045  dicelval3  41935  mapdordlem1a  42389  tfsconcat0i  44055  ismnushort  44994  modelaxreplem2  45671  modelaxreplem3  45672  2reuimp  47835  elpglem3  50474