Theorem anbi2ci 728

Description: Variant of anbi2i 726 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)

Hypothesis

Ref	Expression
anbi.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
anbi2ci	⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))

Proof of Theorem anbi2ci

Step	Hyp	Ref	Expression
1		anbi.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	anbi1i 727	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
3		ancom 465	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
4	2, 3	bitri 263	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  ifpn  1016  clabel  2736  difin0ss  3900  disjxun  4581  asymref  5431  ordpwsuc  6907  supmo  8241  infmo  8284  kmlem3  8857  cfval2  8965  eqger  17467  gaorber  17564  opprunit  18484  xmeter  22048  iscvsp  22736  bj-clabel  31971  clsk1indlem4  37362  usgr2pth0  40971  alimp-no-surprise  42336