Theorem anbi2ci 624

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  clabel  2891  difin0ss  4396  disjxun  5164  elidinxp  6073  cnvresima  6261  ordpwsuc  7851  supmo  9521  infmo  9564  kmlem3  10222  cfval2  10329  eqger  19218  gaorber  19348  opprunit  20403  issubrng  20573  xmeter  24464  iscvsp  25180  elold  27926  usgr2pth0  29801  bj-dfnnf2  36703  funALTVfun  38654  clsk1indlem4  44006  alimp-no-surprise  48875