Theorem anbi2ci 625

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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  ifpnOLD  1073  clabel  2881  difin0ss  4368  disjxun  5146  elidinxp  6043  cnvresima  6229  ordpwsuc  7805  supmo  9449  infmo  9492  kmlem3  10149  cfval2  10257  eqger  19060  gaorber  19174  opprunit  20195  xmeter  23946  iscvsp  24651  elold  27372  usgr2pth0  29060  bj-dfnnf2  35701  funALTVfun  37654  clsk1indlem4  42877  issubrng  46805  alimp-no-surprise  47906