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  3612  rmoan  3701  2reuswap  3708  2reuswap2  3709  reuxfrd  3710  reuind  3715  2rmoswap  3723  sbccomlemOLD  3824  indifdi  4247  elunirab  4876  axsepgfromrep  5236  opeliunxp  5690  elinxp  5974  resoprab  7471  elrnmpores  7491  ov6g  7517  opabex3d  7907  opabex3rd  7908  opabex3  7909  dfrecs3  8302  oeeu  8528  xpassen  8995  omxpenlem  9002  dfac5lem2  10037  ltexprlem4  10952  2clim  15497  divalglem10  16331  bitsmod  16365  isssc  17745  eldmcoa  17990  issubrg  20474  isbasis2g  22851  tgval2  22859  is1stc2  23345  elflim2  23867  i1fres  25622  dvdsflsumcom  27114  vmasum  27143  logfac2  27144  axcontlem2  28928  fusgr2wsp2nb  30296  reuxfrdf  32453  1stpreima  32663  bnj849  34894  elima4  35751  elfuns  35891  dfrecs2  35926  dfrdg4  35927  bj-restuni  37073  bj-imdirco  37166  mptsnunlem  37314  relowlpssretop  37340  poimirlem27  37629  sstotbnd3  37758  an12i  38080  selconj  38082  eldmqsres  38263  inxpxrn  38369  rnxrnres  38373  refrelredund4  38614  islshpat  38998  islpln5  39517  islvol5  39561  cdleme0nex  40272  dicelval3  41162  mapdordlem1a  41616  tfsconcat0i  43321  ismnushort  44277  modelaxreplem2  44956  modelaxreplem3  44957  2reuimp  47103  elpglem3  49702