Theorem an12 370

Description: A rearrangement of conjuncts.

Assertion

Ref	Expression
an12	⊢ ((φ ∧ (ψ ∧ χ)) ↔ (ψ ∧ (φ ∧ χ)))

Proof of Theorem an12

Step	Hyp	Ref	Expression
1		ancom 333	. . 3 ⊢ ((φ ∧ ψ) ↔ (ψ ∧ φ))
2	1	anbi1i 368	. 2 ⊢ (((φ ∧ ψ) ∧ χ) ↔ ((ψ ∧ φ) ∧ χ))
3		anass 336	. 2 ⊢ (((φ ∧ ψ) ∧ χ) ↔ (φ ∧ (ψ ∧ χ)))
4		anass 336	. 2 ⊢ (((ψ ∧ φ) ∧ χ) ↔ (ψ ∧ (φ ∧ χ)))
5	2, 3, 4	3bitr3 156	1 ⊢ ((φ ∧ (ψ ∧ χ)) ↔ (ψ ∧ (φ ∧ χ)))

Syntax hints:   ↔ wb 127   ∧ wa 196

This theorem is referenced by:  an1s 372  an4 388  r19.29 1295  2reuswap 1341  ceqsrexv 1413  zfaus 1480  reuxfr2 1579  dfiun2 2014  elxp2 2443  imaiun 2650  fcoi2 2766  f1o2 2804  f1o5 2808  xpassen 3344  aceq5lem2 3559  distrpq 3861  genpass 3906  ltexprlem4 3939  suppsr2 4017  elreal 4044

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org