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 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  2882  difin0ss  4327  disjxun  5098  elidinxp  6011  cnvresima  6196  ordpwsuc  7767  supmo  9367  infmo  9412  kmlem3  10075  cfval2  10182  eqger  19119  gaorber  19249  opprunit  20325  issubrng  20492  xmeter  24389  iscvsp  25096  elold  27867  usgr2pth0  29850  axregs  35314  bj-dfnnf2  36976  funALTVfun  39028  clsk1indlem4  44394  alimp-no-surprise  50134