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 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  2874  difin0ss  4326  disjxun  5093  elidinxp  5999  cnvresima  6183  ordpwsuc  7754  supmo  9361  infmo  9406  kmlem3  10066  cfval2  10173  eqger  19075  gaorber  19205  opprunit  20280  issubrng  20450  xmeter  24337  iscvsp  25044  elold  27801  usgr2pth0  29728  axregs  35073  bj-dfnnf2  36710  funALTVfun  38675  clsk1indlem4  44017  alimp-no-surprise  49767