Theorem an12 855

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 465	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
2	1	anbi1i 731	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜓 ∧ 𝜑) ∧ 𝜒))
3		anass 682	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
4		anass 682	. 2 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
5	2, 3, 4	3bitr3i 290	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  an32  856  an13  857  an12s  860  an4  882  ceqsrexv  3367  rmoan  3439  2reuswap  3443  reuind  3444  sbccomlem  3541  elunirab  4480  axsep  4813  reuxfr2d  4921  opeliunxp  5204  elres  5470  resoprab  6798  elrnmpt2res  6816  ov6g  6840  opabex3d  7187  opabex3  7188  dfrecs3  7514  oeeu  7728  xpassen  8095  omxpenlem  8102  dfac5lem2  8985  ltexprlem4  9899  rexuz2  11777  2clim  14347  divalglem10  15172  bitsmod  15205  isssc  16527  eldmcoa  16762  issubrg  18828  isbasis2g  20800  tgval2  20808  is1stc2  21293  elflim2  21815  i1fres  23517  dvdsflsumcom  24959  vmasum  24986  logfac2  24987  axcontlem2  25890  fusgr2wsp2nb  27314  2reuswap2  29455  reuxfr3d  29456  1stpreima  29612  bnj849  31121  elima4  31803  elfuns  32147  brimg  32169  dfrecs2  32182  dfrdg4  32183  bj-axsep  32918  bj-restuni  33175  mptsnunlem  33315  relowlpssretop  33342  poimirlem27  33566  sstotbnd3  33705  an12i  34030  selconj  34032  eldmqsres  34192  inxpxrn  34293  rnxrnres  34297  islshpat  34622  islpln5  35139  islvol5  35183  cdleme0nex  35895  dicelval3  36786  mapdordlem1a  37240  2rmoswap  41505  elpglem3  42784