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  3606  rmoan  3694  2reuswap  3701  2reuswap2  3702  reuxfrd  3703  reuind  3708  2rmoswap  3716  sbccomlemOLD  3817  indifdi  4243  elunirab  4873  axsepgfromrep  5234  opeliunxp  5686  elinxp  5972  resoprab  7470  elrnmpores  7490  ov6g  7516  opabex3d  7903  opabex3rd  7904  opabex3  7905  dfrecs3  8298  oeeu  8524  xpassen  8991  omxpenlem  8998  dfac5lem2  10022  ltexprlem4  10937  2clim  15481  divalglem10  16315  bitsmod  16349  isssc  17729  eldmcoa  17974  issubrg  20488  isbasis2g  22864  tgval2  22872  is1stc2  23358  elflim2  23880  i1fres  25634  dvdsflsumcom  27126  vmasum  27155  logfac2  27156  axcontlem2  28945  fusgr2wsp2nb  30316  reuxfrdf  32472  1stpreima  32692  bnj849  34958  elima4  35841  elfuns  35978  dfrecs2  36015  dfrdg4  36016  bj-restuni  37162  bj-imdirco  37255  mptsnunlem  37403  relowlpssretop  37429  poimirlem27  37707  sstotbnd3  37836  an12i  38158  selconj  38160  eldmqsres  38345  inxpxrn  38462  rnxrnres  38466  refrelredund4  38751  islshpat  39136  islpln5  39654  islvol5  39698  cdleme0nex  40409  dicelval3  41299  mapdordlem1a  41753  tfsconcat0i  43462  ismnushort  44418  modelaxreplem2  45096  modelaxreplem3  45097  2reuimp  47239  elpglem3  49838