Theorem an12 873

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 733	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜓 ∧ 𝜑) ∧ 𝜒))
3		anass 684	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
4		anass 684	. 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  874  an13  875  an12s  878  an4  900  3anan12  1082  ceqsrexv  3475  rmoan  3547  2reuswap  3551  reuind  3552  sbccomlem  3649  elunirab  4600  axsep  4932  reuxfr2d  5040  opeliunxp  5327  elres  5593  resoprab  6922  elrnmpt2res  6940  ov6g  6964  opabex3d  7311  opabex3  7312  dfrecs3  7639  oeeu  7854  xpassen  8221  omxpenlem  8228  dfac5lem2  9157  ltexprlem4  10073  rexuz2  11952  2clim  14522  divalglem10  15347  bitsmod  15380  isssc  16701  eldmcoa  16936  issubrg  19002  isbasis2g  20974  tgval2  20982  is1stc2  21467  elflim2  21989  i1fres  23691  dvdsflsumcom  25134  vmasum  25161  logfac2  25162  axcontlem2  26065  fusgr2wsp2nb  27509  2reuswap2  29657  reuxfr3d  29658  1stpreima  29814  bnj849  31323  elima4  32005  elfuns  32349  brimg  32371  dfrecs2  32384  dfrdg4  32385  bj-axsep  33121  bj-restuni  33374  mptsnunlem  33514  relowlpssretop  33541  poimirlem27  33767  sstotbnd3  33906  an12i  34231  selconj  34233  eldmqsres  34393  inxpxrn  34494  rnxrnres  34498  islshpat  34825  islpln5  35342  islvol5  35386  cdleme0nex  36098  dicelval3  36989  mapdordlem1a  37443  2rmoswap  41708  elpglem3  42987