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  3641  rmoan  3733  2reuswap  3740  2reuswap2  3741  reuxfrd  3742  reuind  3747  2rmoswap  3755  sbccomlem  3862  indifdi  4281  elunirab  4920  axsepgfromrep  5293  opeliunxp  5738  elinxp  6014  resoprab  7513  elrnmpores  7533  ov6g  7558  opabex3d  7939  opabex3rd  7940  opabex3  7941  dfrecs3  8359  dfrecs3OLD  8360  oeeu  8591  xpassen  9054  omxpenlem  9061  dfac5lem2  10106  ltexprlem4  11021  2clim  15503  divalglem10  16332  bitsmod  16364  isssc  17754  eldmcoa  18002  issubrg  20340  isbasis2g  22420  tgval2  22428  is1stc2  22915  elflim2  23437  i1fres  25192  dvdsflsumcom  26659  vmasum  26686  logfac2  26687  axcontlem2  28190  fusgr2wsp2nb  29554  reuxfrdf  31696  1stpreima  31899  bnj849  33867  elima4  34678  elfuns  34818  dfrecs2  34853  dfrdg4  34854  bj-restuni  35883  bj-imdirco  35976  mptsnunlem  36124  relowlpssretop  36150  poimirlem27  36420  sstotbnd3  36550  an12i  36872  selconj  36874  eldmqsres  37061  inxpxrn  37171  rnxrnres  37175  refrelredund4  37411  islshpat  37793  islpln5  38312  islvol5  38356  cdleme0nex  39067  dicelval3  39957  mapdordlem1a  40411  tfsconcat0i  41966  ismnushort  42931  2reuimp  45696  elpglem3  47598