Theorem an12 561

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 266	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
2	1	anbi1i 458	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜓 ∧ 𝜑) ∧ 𝜒))
3		anass 401	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
4		anass 401	. 2 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
5	2, 3, 4	3bitr3i 210	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an32  562  an13  563  an12s  565  an4  586  ceqsrexv  2905  rmoan  2975  2reuswapdc  2979  reuind  2980  2rmorex  2981  sbccomlem  3075  elunirab  3866  rexxfrd  4515  opeliunxp  4735  elres  5001  resoprab  6051  ov6g  6094  opabex3d  6216  opabex3  6217  xpassen  6937  distrnqg  7513  distrnq0  7585  rexuz2  9715  2clim  11662  bitsmod  12317  issubrg  14033  isbasis2g  14567  tgval2  14573