Theorem an12 651

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 461	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
2	1	bianass 648	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	2	biancomi 463	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  an12s  655  an4  662  3anan12  1101  ceqsrexv  3600  rmoan  3687  2reuswap  3694  2reuswap2  3695  reuxfrd  3696  reuind  3701  2rmoswap  3709  sbccomlemOLD  3809  indifdi  4229  elunirab  4860  axsepgfromrep  5223  opeliunxp  5692  elinxp  5978  resoprab  7481  elrnmpores  7501  ov6g  7527  opabex3d  7914  opabex3rd  7915  opabex3  7916  dfrecs3  8309  oeeu  8536  xpassen  9006  omxpenlem  9013  dfac5lem2  10044  ltexprlem4  10960  2clim  15532  divalglem10  16369  bitsmod  16403  isssc  17785  eldmcoa  18030  issubrg  20550  isbasis2g  22938  tgval2  22946  is1stc2  23432  elflim2  23954  i1fres  25697  dvdsflsumcom  27176  vmasum  27204  logfac2  27205  axcontlem2  29059  fusgr2wsp2nb  30429  reuxfrdf  32585  1stpreima  32806  bnj849  35114  elima4  36011  elfuns  36148  dfrecs2  36185  dfrdg4  36186  bj-restuni  37462  bj-imdirco  37557  mptsnunlem  37707  relowlpssretop  37733  poimirlem27  38021  sstotbnd3  38150  an12i  38472  selconj  38474  eldmqsres  38667  inxpxrn  38792  rnxrnres  38796  refrelredund4  39093  islshpat  39516  islpln5  40034  islvol5  40078  cdleme0nex  40789  dicelval3  41679  mapdordlem1a  42133  tfsconcat0i  43797  ismnushort  44752  modelaxreplem2  45430  modelaxreplem3  45431  2reuimp  47585  elpglem3  50210