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  2881  difin0ss  4313  disjxun  5083  elidinxp  6009  cnvresima  6194  ordpwsuc  7766  supmo  9365  infmo  9410  kmlem3  10075  cfval2  10182  eqger  19153  gaorber  19283  opprunit  20357  issubrng  20524  xmeter  24398  iscvsp  25095  elold  27851  usgr2pth0  29833  axregs  35283  mh-infprim2bi  36729  mh-infprim3bi  36730  bj-dfnnf2  37036  funALTVfun  39104  clsk1indlem4  44471  alimp-no-surprise  50256