Theorem an12 658

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an12s  662  an4  669  3anan12  1112  ceqsrexv  3612  rmoan  3700  2reuswap  3707  2reuswap2  3708  reuxfrd  3709  reuind  3714  2rmoswap  3722  indifdi  4243  elunirab  4885  axsepgfromrep  5253  opeliunxp  5726  elinxp  6016  resoprab  7535  elrnmpores  7555  ov6g  7581  opabex3d  7966  opabex3rd  7967  opabex3  7968  dfrecs3  8365  oeeu  8595  xpassen  9073  omxpenlem  9080  dfac5lem2  10131  ltexprlem4  11052  2clim  15663  divalglem10  16498  bitsmod  16532  isssc  17915  eldmcoa  18160  issubrg  20739  isbasis2g  23179  tgval2  23187  is1stc2  23673  elflim2  24196  i1fres  25939  dvdsflsumcom  27432  vmasum  27460  logfac2  27461  axcontlem2  29430  fusgr2wsp2nb  30822  reuxfrdf  32974  1stpreima  33187  bnj849  35442  elima4  36363  elfuns  36500  dfrecs2  36537  dfrdg4  36538  bj-restuni  37855  bj-imdirco  37950  mptsnunlem  38100  relowlpssretop  38126  poimirlem27  38404  sstotbnd3  38534  an12i  38854  selconj  38856  eldmqsres  39049  inxpxrn  39174  rnxrnres  39178  refrelredund4  39475  islshpat  39898  islpln5  40416  islvol5  40460  cdleme0nex  41171  dicelval3  42061  mapdordlem1a  42515  tfsconcat0i  44194  ismnushort  45133  modelaxreplem2  45810  modelaxreplem3  45811  2reuimp  48011  elpglem3  50647