Theorem an12 641

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

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  an12s  645  an4  652  3anan12  1094  ceqsrexv  3578  rmoan  3669  2reuswap  3676  2reuswap2  3677  reuxfrd  3678  reuind  3683  2rmoswap  3691  sbccomlem  3799  indifdi  4214  elunirab  4852  axsepgfromrep  5216  opeliunxp  5645  elinxp  5918  resoprab  7370  elrnmpores  7389  ov6g  7414  opabex3d  7781  opabex3rd  7782  opabex3  7783  dfrecs3  8174  dfrecs3OLD  8175  oeeu  8396  xpassen  8806  omxpenlem  8813  dfac5lem2  9811  ltexprlem4  10726  2clim  15209  divalglem10  16039  bitsmod  16071  isssc  17449  eldmcoa  17696  issubrg  19939  isbasis2g  22006  tgval2  22014  is1stc2  22501  elflim2  23023  i1fres  24775  dvdsflsumcom  26242  vmasum  26269  logfac2  26270  axcontlem2  27236  fusgr2wsp2nb  28599  reuxfrdf  30740  1stpreima  30941  bnj849  32805  elima4  33656  elfuns  34144  dfrecs2  34179  dfrdg4  34180  bj-restuni  35195  bj-imdirco  35288  mptsnunlem  35436  relowlpssretop  35462  poimirlem27  35731  sstotbnd3  35861  an12i  36183  selconj  36185  eldmqsres  36348  inxpxrn  36448  rnxrnres  36452  refrelredund4  36675  islshpat  36958  islpln5  37476  islvol5  37520  cdleme0nex  38231  dicelval3  39121  mapdordlem1a  39575  ismnushort  41808  2reuimp  44494  elpglem3  46304