Theorem an12 658

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an12s  662  an4  669  3anan12  1112  ceqsrexv  3608  rmoan  3696  2reuswap  3703  2reuswap2  3704  reuxfrd  3705  reuind  3710  2rmoswap  3718  indifdi  4239  elunirab  4881  axsepgfromrep  5246  opeliunxp  5717  elinxp  6007  resoprab  7538  elrnmpores  7558  ov6g  7584  funmpt3  7687  mpt3fvd  7688  opabex3d  7977  opabex3rd  7978  opabex3  7979  dfrecs3  8383  oeeu  8615  xpassen  9093  omxpenlem  9100  dfac5lem2  10206  ltexprlem4  11127  2clim  15744  divalglem10  16577  bitsmod  16611  isssc  18000  eldmcoa  18245  issubrg  20828  isbasis2g  23271  tgval2  23279  is1stc2  23765  elflim2  24288  i1fres  26031  dvdsflsumcom  27520  vmasum  27548  logfac2  27549  axcontlem2  29548  fusgr2wsp2nb  30940  reuxfrdf  33134  1stpreima  33347  bnj849  35601  elima4  36632  elfuns  36769  dfrecs2  36806  dfrdg4  36807  bj-restuni  38110  bj-imdirco  38204  mptsnunlem  38354  relowlpssretop  38380  poimirlem27  38658  sstotbnd3  38803  an12i  39123  selconj  39125  eldmqsres  39318  inxpxrn  39443  rnxrnres  39447  refrelredund4  39744  islshpat  40167  islpln5  40685  islvol5  40729  cdleme0nex  41440  dicelval3  42330  mapdordlem1a  42784  tfsconcat0i  44440  ismnushort  45378  modelaxreplem2  46062  modelaxreplem3  46063  2reuimp  48278  elpglem3  50974