Theorem anbi2ci 626

Description: Variant of anbi2i 624 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 625	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
3	2	biancomi 465	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ifpn  1067  clabel  2959  difin0ss  4328  disjxun  5064  elidinxp  5911  cnvresima  6087  ordpwsuc  7530  supmo  8916  infmo  8959  kmlem3  9578  cfval2  9682  eqger  18330  gaorber  18438  opprunit  19411  xmeter  23043  iscvsp  23732  usgr2pth0  27546  bj-dfnnf2  34066  funALTVfun  35946  clsk1indlem4  40414  alimp-no-surprise  44902