Theorem an12 644

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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  an12s  648  an4  655  3anan12  1097  ceqsrexv  3643  rmoan  3735  2reuswap  3742  2reuswap2  3743  reuxfrd  3744  reuind  3749  2rmoswap  3757  sbccomlem  3864  indifdi  4283  elunirab  4924  axsepgfromrep  5297  opeliunxp  5742  elinxp  6018  resoprab  7523  elrnmpores  7543  ov6g  7568  opabex3d  7949  opabex3rd  7950  opabex3  7951  dfrecs3  8369  dfrecs3OLD  8370  oeeu  8600  xpassen  9063  omxpenlem  9070  dfac5lem2  10116  ltexprlem4  11031  2clim  15513  divalglem10  16342  bitsmod  16374  isssc  17764  eldmcoa  18012  issubrg  20356  isbasis2g  22443  tgval2  22451  is1stc2  22938  elflim2  23460  i1fres  25215  dvdsflsumcom  26682  vmasum  26709  logfac2  26710  axcontlem2  28213  fusgr2wsp2nb  29577  reuxfrdf  31719  1stpreima  31916  bnj849  33925  elima4  34736  elfuns  34876  dfrecs2  34911  dfrdg4  34912  bj-restuni  35967  bj-imdirco  36060  mptsnunlem  36208  relowlpssretop  36234  poimirlem27  36504  sstotbnd3  36633  an12i  36955  selconj  36957  eldmqsres  37144  inxpxrn  37254  rnxrnres  37258  refrelredund4  37494  islshpat  37876  islpln5  38395  islvol5  38439  cdleme0nex  39150  dicelval3  40040  mapdordlem1a  40494  tfsconcat0i  42081  ismnushort  43046  2reuimp  45810  elpglem3  47712