Theorem an12 833

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.)

Assertion

Ref	Expression
an12	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Proof of Theorem an12

Step	Hyp	Ref	Expression
1		ancom 464	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
2	1	anbi1i 726	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜓 ∧ 𝜑) ∧ 𝜒))
3		anass 678	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
4		anass 678	. 2 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
5	2, 3, 4	3bitr3i 288	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 194   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  an32  834  an13  835  an12s  838  an4  860  ceqsrexv  3305  rmoan  3372  2reuswap  3376  reuind  3377  sbccomlem  3474  elunirab  4378  axsep  4702  reuxfr2d  4811  opeliunxp  5082  elres  5341  resoprab  6631  elrnmpt2res  6649  ov6g  6673  opabex3d  7014  opabex3  7015  dfrecs3  7333  oeeu  7547  xpassen  7916  omxpenlem  7923  dfac5lem2  8807  ltexprlem4  9717  rexuz2  11573  2clim  14099  divalglem10  14911  bitsmod  14944  isssc  16251  eldmcoa  16486  issubrg  18551  isbasis2g  20510  tgval2  20518  is1stc2  21002  elflim2  21525  i1fres  23222  dvdsflsumcom  24658  vmasum  24685  logfac2  24686  axcontlem2  25590  2reuswap2  28505  reuxfr3d  28506  1stpreima  28660  bnj849  30042  elima4  30717  nofulllem5  30898  elfuns  30985  brimg  31007  dfrecs2  31020  dfrdg4  31021  bj-axsep  31774  bj-restuni  32014  mptsnunlem  32144  relowlpssretop  32171  poimirlem27  32389  sstotbnd3  32528  an12i  32853  selconj  32855  islshpat  33105  islpln5  33622  islvol5  33666  cdleme0nex  34378  dicelval3  35270  mapdordlem1a  35724  2rmoswap  39616