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  3654  rmoan  3747  2reuswap  3754  2reuswap2  3755  reuxfrd  3756  reuind  3761  2rmoswap  3769  sbccomlemOLD  3878  indifdi  4299  elunirab  4926  axsepgfromrep  5299  opeliunxp  5755  elinxp  6038  resoprab  7550  elrnmpores  7570  ov6g  7596  opabex3d  7988  opabex3rd  7989  opabex3  7990  dfrecs3  8410  dfrecs3OLD  8411  oeeu  8639  xpassen  9104  omxpenlem  9111  dfac5lem2  10161  ltexprlem4  11076  2clim  15604  divalglem10  16435  bitsmod  16469  isssc  17867  eldmcoa  18118  issubrg  20587  isbasis2g  22970  tgval2  22978  is1stc2  23465  elflim2  23987  i1fres  25754  dvdsflsumcom  27245  vmasum  27274  logfac2  27275  axcontlem2  28994  fusgr2wsp2nb  30362  reuxfrdf  32518  1stpreima  32721  bnj849  34917  elima4  35756  elfuns  35896  dfrecs2  35931  dfrdg4  35932  bj-restuni  37079  bj-imdirco  37172  mptsnunlem  37320  relowlpssretop  37346  poimirlem27  37633  sstotbnd3  37762  an12i  38084  selconj  38086  eldmqsres  38268  inxpxrn  38376  rnxrnres  38380  refrelredund4  38616  islshpat  38998  islpln5  39517  islvol5  39561  cdleme0nex  40272  dicelval3  41162  mapdordlem1a  41616  tfsconcat0i  43334  ismnushort  44296  modelaxreplem2  44943  modelaxreplem3  44944  2reuimp  47064  elpglem3  48943