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  1110  ceqsrexv  3617  rmoan  3705  2reuswap  3712  2reuswap2  3713  reuxfrd  3714  reuind  3719  2rmoswap  3727  sbccomlemOLD  3826  indifdi  4249  elunirab  4882  axsepgfromrep  5248  opeliunxp  5718  elinxp  6008  resoprab  7518  elrnmpores  7538  ov6g  7564  opabex3d  7950  opabex3rd  7951  opabex3  7952  dfrecs3  8347  oeeu  8577  xpassen  9047  omxpenlem  9054  dfac5lem2  10096  ltexprlem4  11012  2clim  15611  divalglem10  16448  bitsmod  16482  isssc  17865  eldmcoa  18110  issubrg  20644  isbasis2g  23062  tgval2  23070  is1stc2  23556  elflim2  24078  i1fres  25821  dvdsflsumcom  27306  vmasum  27334  logfac2  27335  axcontlem2  29220  fusgr2wsp2nb  30590  reuxfrdf  32743  1stpreima  32960  bnj849  35225  elima4  36134  elfuns  36271  dfrecs2  36308  dfrdg4  36309  bj-restuni  37594  bj-imdirco  37689  mptsnunlem  37839  relowlpssretop  37865  poimirlem27  38153  sstotbnd3  38282  an12i  38604  selconj  38606  eldmqsres  38799  inxpxrn  38924  rnxrnres  38928  refrelredund4  39225  islshpat  39648  islpln5  40166  islvol5  40210  cdleme0nex  40921  dicelval3  41811  mapdordlem1a  42265  tfsconcat0i  43929  ismnushort  44870  modelaxreplem2  45547  modelaxreplem3  45548  2reuimp  47708  elpglem3  50343