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  3612  rmoan  3700  2reuswap  3707  2reuswap2  3708  reuxfrd  3709  reuind  3714  2rmoswap  3722  indifdi  4242  elunirab  4885  axsepgfromrep  5250  opeliunxp  5722  elinxp  6020  resoprab  7561  elrnmpores  7582  ov6g  7608  funmpt3  7711  mpt3fvd  7712  opabex3d  8001  opabex3rd  8002  opabex3  8003  dfrecs3  8408  oeeu  8640  xpassen  9118  omxpenlem  9125  dfac5lem2  10230  ltexprlem4  11151  2clim  15768  divalglem10  16601  bitsmod  16635  isssc  18024  eldmcoa  18269  issubrg  20853  isbasis2g  23296  tgval2  23304  is1stc2  23790  elflim2  24313  i1fres  26056  dvdsflsumcom  27545  vmasum  27573  logfac2  27574  axcontlem2  29573  fusgr2wsp2nb  30965  reuxfrdf  33159  1stpreima  33371  bnj849  35625  elima4  36718  elfuns  36855  dfrecs2  36892  dfrdg4  36893  bj-dfres2  38141  bj-restuni  38209  bj-imdirco  38303  mptsnunlem  38453  relowlpssretop  38479  poimirlem27  38757  sstotbnd3  38902  an12i  39222  selconj  39224  eldmqsres  39417  inxpxrn  39542  rnxrnres  39546  refrelredund4  39843  islshpat  40266  islpln5  40784  islvol5  40828  cdleme0nex  41539  dicelval3  42429  mapdordlem1a  42883  tfsconcat0i  44539  ismnushort  45477  modelaxreplem2  46164  modelaxreplem3  46165  2reuimp  48391  elpglem3  51086