Theorem an12 644

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 464	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
2	1	bianass 641	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	2	biancomi 466	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 209   ∧ wa 399

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 400

This theorem is referenced by:  an12s  648  an4  655  3anan12  1093  ceqsrexv  3597  rmoan  3678  2reuswap  3685  2reuswap2  3686  reuxfrd  3687  reuind  3692  2rmoswap  3700  sbccomlem  3799  elunirab  4816  axsepgfromrep  5165  opeliunxp  5583  elinxp  5856  resoprab  7249  elrnmpores  7267  ov6g  7292  opabex3d  7648  opabex3rd  7649  opabex3  7650  dfrecs3  7992  oeeu  8212  xpassen  8594  omxpenlem  8601  dfac5lem2  9535  ltexprlem4  10450  2clim  14921  divalglem10  15743  bitsmod  15775  isssc  17082  eldmcoa  17317  issubrg  19528  isbasis2g  21553  tgval2  21561  is1stc2  22047  elflim2  22569  i1fres  24309  dvdsflsumcom  25773  vmasum  25800  logfac2  25801  axcontlem2  26759  fusgr2wsp2nb  28119  reuxfrdf  30262  1stpreima  30466  bnj849  32307  elima4  33132  elfuns  33489  dfrecs2  33524  dfrdg4  33525  bj-restuni  34512  bj-imdirco  34605  mptsnunlem  34755  relowlpssretop  34781  poimirlem27  35084  sstotbnd3  35214  an12i  35536  selconj  35538  eldmqsres  35703  inxpxrn  35803  rnxrnres  35807  refrelredund4  36030  islshpat  36313  islpln5  36831  islvol5  36875  cdleme0nex  37586  dicelval3  38476  mapdordlem1a  38930  2reuimp  43671  elpglem3  45242