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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  an12s  649  an4  656  3anan12  1094  ceqsrexv  3565  rmoan  3650  2reuswap  3657  2reuswap2  3658  reuxfrd  3659  reuind  3664  2rmoswap  3672  sbccomlem  3772  indifdi  4184  elunirab  4807  axsepgfromrep  5160  opeliunxp  5581  elinxp  5854  resoprab  7257  elrnmpores  7276  ov6g  7301  opabex3d  7663  opabex3rd  7664  opabex3  7665  dfrecs3  8012  oeeu  8232  xpassen  8624  omxpenlem  8631  dfac5lem2  9569  ltexprlem4  10484  2clim  14962  divalglem10  15788  bitsmod  15820  isssc  17134  eldmcoa  17376  issubrg  19588  isbasis2g  21633  tgval2  21641  is1stc2  22127  elflim2  22649  i1fres  24390  dvdsflsumcom  25857  vmasum  25884  logfac2  25885  axcontlem2  26843  fusgr2wsp2nb  28203  reuxfrdf  30346  1stpreima  30548  bnj849  32410  elima4  33251  elfuns  33751  dfrecs2  33786  dfrdg4  33787  bj-restuni  34777  bj-imdirco  34870  mptsnunlem  35020  relowlpssretop  35046  poimirlem27  35349  sstotbnd3  35479  an12i  35801  selconj  35803  eldmqsres  35968  inxpxrn  36068  rnxrnres  36072  refrelredund4  36295  islshpat  36578  islpln5  37096  islvol5  37140  cdleme0nex  37851  dicelval3  38741  mapdordlem1a  39195  2reuimp  44024  elpglem3  45592