Theorem an12 495

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 253	. . 3 ⊢ ((φ ∧ ψ) ↔ (ψ ∧ φ))
2	1	anbi1i 431	. 2 ⊢ (((φ ∧ ψ) ∧ χ) ↔ ((ψ ∧ φ) ∧ χ))
3		anass 381	. 2 ⊢ (((φ ∧ ψ) ∧ χ) ↔ (φ ∧ (ψ ∧ χ)))
4		anass 381	. 2 ⊢ (((ψ ∧ φ) ∧ χ) ↔ (ψ ∧ (φ ∧ χ)))
5	2, 3, 4	3bitr3i 199	1 ⊢ ((φ ∧ (ψ ∧ χ)) ↔ (ψ ∧ (φ ∧ χ)))

Syntax hints:   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  an32  496  an13  497  an12s  499  an4  520  ceqsrexv  2668  rmoan  2733  2reuswapdc  2737  reuind  2738  2rmorex  2739  sbccomlem  2826  elunirab  3584  rexxfrd  4161  opeliunxp  4338  elres  4589  resoprab  5539  ov6g  5580  opabex3d  5690  opabex3  5691  xpassen  6240  distrnqg  6371  distrnq0  6442  rexuz2  8300