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  3610  rmoan  3698  2reuswap  3705  2reuswap2  3706  reuxfrd  3707  reuind  3712  2rmoswap  3720  sbccomlemOLD  3821  indifdi  4244  elunirab  4874  axsepgfromrep  5232  opeliunxp  5683  elinxp  5968  resoprab  7464  elrnmpores  7484  ov6g  7510  opabex3d  7897  opabex3rd  7898  opabex3  7899  dfrecs3  8292  oeeu  8518  xpassen  8984  omxpenlem  8991  dfac5lem2  10015  ltexprlem4  10930  2clim  15479  divalglem10  16313  bitsmod  16347  isssc  17727  eldmcoa  17972  issubrg  20487  isbasis2g  22864  tgval2  22872  is1stc2  23358  elflim2  23880  i1fres  25634  dvdsflsumcom  27126  vmasum  27155  logfac2  27156  axcontlem2  28944  fusgr2wsp2nb  30312  reuxfrdf  32468  1stpreima  32686  bnj849  34935  elima4  35818  elfuns  35955  dfrecs2  35990  dfrdg4  35991  bj-restuni  37137  bj-imdirco  37230  mptsnunlem  37378  relowlpssretop  37404  poimirlem27  37693  sstotbnd3  37822  an12i  38144  selconj  38146  eldmqsres  38327  inxpxrn  38433  rnxrnres  38437  refrelredund4  38678  islshpat  39062  islpln5  39580  islvol5  39624  cdleme0nex  40335  dicelval3  41225  mapdordlem1a  41679  tfsconcat0i  43384  ismnushort  44340  modelaxreplem2  45018  modelaxreplem3  45019  2reuimp  47152  elpglem3  49751