Theorem anbi2ci 634

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

Syntax hints:   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  clabel  2906  difin0ss  4325  disjxun  5097  elidinxp  6030  cnvresima  6213  ordpwsuc  7791  supmo  9395  infmo  9440  kmlem3  10106  cfval2  10214  eqger  19202  gaorber  19331  opprunit  20405  issubrng  20576  xmeter  24473  iscvsp  25170  elold  27929  usgr2pth0  29911  axregs  35399  mh-infprim2bi  36871  mh-infprim3bi  36872  bj-dfnnf2  37178  funALTVfun  39246  clsk1indlem4  44584  alimp-no-surprise  50366