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  3609  rmoan  3697  2reuswap  3704  2reuswap2  3705  reuxfrd  3706  reuind  3711  2rmoswap  3719  indifdi  4240  elunirab  4882  axsepgfromrep  5247  opeliunxp  5718  elinxp  6010  resoprab  7530  elrnmpores  7550  ov6g  7576  funmpt3  7679  opabex3d  7966  opabex3rd  7967  opabex3  7968  dfrecs3  8364  oeeu  8596  xpassen  9074  omxpenlem  9081  dfac5lem2  10184  ltexprlem4  11105  2clim  15719  divalglem10  16552  bitsmod  16586  isssc  17975  eldmcoa  18220  issubrg  20803  isbasis2g  23246  tgval2  23254  is1stc2  23740  elflim2  24263  i1fres  26006  dvdsflsumcom  27497  vmasum  27525  logfac2  27526  axcontlem2  29525  fusgr2wsp2nb  30917  reuxfrdf  33069  1stpreima  33282  bnj849  35538  elima4  36510  elfuns  36647  dfrecs2  36684  dfrdg4  36685  bj-restuni  37986  bj-imdirco  38079  mptsnunlem  38229  relowlpssretop  38255  poimirlem27  38533  sstotbnd3  38678  an12i  38998  selconj  39000  eldmqsres  39193  inxpxrn  39318  rnxrnres  39322  refrelredund4  39619  islshpat  40042  islpln5  40560  islvol5  40604  cdleme0nex  41315  dicelval3  42205  mapdordlem1a  42659  tfsconcat0i  44305  ismnushort  45244  modelaxreplem2  45921  modelaxreplem3  45922  2reuimp  48129  elpglem3  50750