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  4336  disjxun  5105  elidinxp  6015  cnvresima  6203  ordpwsuc  7790  supmo  9403  infmo  9448  kmlem3  10106  cfval2  10213  eqger  19110  gaorber  19240  opprunit  20286  issubrng  20456  xmeter  24321  iscvsp  25028  elold  27781  usgr2pth0  29695  bj-dfnnf2  36725  funALTVfun  38690  clsk1indlem4  44033  alimp-no-surprise  49767