Theorem an12 646

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

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

This theorem is referenced by:  an12s  650  an4  657  3anan12  1096  ceqsrexv  3598  rmoan  3686  2reuswap  3693  2reuswap2  3694  reuxfrd  3695  reuind  3700  2rmoswap  3708  sbccomlemOLD  3809  indifdi  4235  elunirab  4866  axsepgfromrep  5229  opeliunxp  5691  elinxp  5978  resoprab  7478  elrnmpores  7498  ov6g  7524  opabex3d  7911  opabex3rd  7912  opabex3  7913  dfrecs3  8305  oeeu  8532  xpassen  9002  omxpenlem  9009  dfac5lem2  10037  ltexprlem4  10953  2clim  15525  divalglem10  16362  bitsmod  16396  isssc  17778  eldmcoa  18023  issubrg  20539  isbasis2g  22923  tgval2  22931  is1stc2  23417  elflim2  23939  i1fres  25682  dvdsflsumcom  27165  vmasum  27193  logfac2  27194  axcontlem2  29048  fusgr2wsp2nb  30419  reuxfrdf  32575  1stpreima  32795  bnj849  35083  elima4  35974  elfuns  36111  dfrecs2  36148  dfrdg4  36149  bj-restuni  37425  bj-imdirco  37520  mptsnunlem  37668  relowlpssretop  37694  poimirlem27  37982  sstotbnd3  38111  an12i  38433  selconj  38435  eldmqsres  38628  inxpxrn  38753  rnxrnres  38757  refrelredund4  39054  islshpat  39477  islpln5  39995  islvol5  40039  cdleme0nex  40750  dicelval3  41640  mapdordlem1a  42094  tfsconcat0i  43791  ismnushort  44746  modelaxreplem2  45424  modelaxreplem3  45425  2reuimp  47575  elpglem3  50200