Theorem an12 645

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 642	. 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  649  an4  656  3anan12  1095  ceqsrexv  3621  rmoan  3710  2reuswap  3717  2reuswap2  3718  reuxfrd  3719  reuind  3724  2rmoswap  3732  sbccomlemOLD  3833  indifdi  4257  elunirab  4886  axsepgfromrep  5249  opeliunxp  5705  elinxp  5990  resoprab  7507  elrnmpores  7527  ov6g  7553  opabex3d  7944  opabex3rd  7945  opabex3  7946  dfrecs3  8341  oeeu  8567  xpassen  9035  omxpenlem  9042  dfac5lem2  10077  ltexprlem4  10992  2clim  15538  divalglem10  16372  bitsmod  16406  isssc  17782  eldmcoa  18027  issubrg  20480  isbasis2g  22835  tgval2  22843  is1stc2  23329  elflim2  23851  i1fres  25606  dvdsflsumcom  27098  vmasum  27127  logfac2  27128  axcontlem2  28892  fusgr2wsp2nb  30263  reuxfrdf  32420  1stpreima  32630  bnj849  34915  elima4  35763  elfuns  35903  dfrecs2  35938  dfrdg4  35939  bj-restuni  37085  bj-imdirco  37178  mptsnunlem  37326  relowlpssretop  37352  poimirlem27  37641  sstotbnd3  37770  an12i  38092  selconj  38094  eldmqsres  38275  inxpxrn  38381  rnxrnres  38385  refrelredund4  38626  islshpat  39010  islpln5  39529  islvol5  39573  cdleme0nex  40284  dicelval3  41174  mapdordlem1a  41628  tfsconcat0i  43334  ismnushort  44290  modelaxreplem2  44969  modelaxreplem3  44970  2reuimp  47116  elpglem3  49702