Theorem an12 645

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  an12s  649  an4  656  3anan12  1095  ceqsrexv  3624  rmoan  3713  2reuswap  3720  2reuswap2  3721  reuxfrd  3722  reuind  3727  2rmoswap  3735  sbccomlemOLD  3836  indifdi  4260  elunirab  4889  axsepgfromrep  5252  opeliunxp  5708  elinxp  5993  resoprab  7510  elrnmpores  7530  ov6g  7556  opabex3d  7947  opabex3rd  7948  opabex3  7949  dfrecs3  8344  oeeu  8570  xpassen  9040  omxpenlem  9047  dfac5lem2  10084  ltexprlem4  10999  2clim  15545  divalglem10  16379  bitsmod  16413  isssc  17789  eldmcoa  18034  issubrg  20487  isbasis2g  22842  tgval2  22850  is1stc2  23336  elflim2  23858  i1fres  25613  dvdsflsumcom  27105  vmasum  27134  logfac2  27135  axcontlem2  28899  fusgr2wsp2nb  30270  reuxfrdf  32427  1stpreima  32637  bnj849  34922  elima4  35770  elfuns  35910  dfrecs2  35945  dfrdg4  35946  bj-restuni  37092  bj-imdirco  37185  mptsnunlem  37333  relowlpssretop  37359  poimirlem27  37648  sstotbnd3  37777  an12i  38099  selconj  38101  eldmqsres  38282  inxpxrn  38388  rnxrnres  38392  refrelredund4  38633  islshpat  39017  islpln5  39536  islvol5  39580  cdleme0nex  40291  dicelval3  41181  mapdordlem1a  41635  tfsconcat0i  43341  ismnushort  44297  modelaxreplem2  44976  modelaxreplem3  44977  2reuimp  47120  elpglem3  49706