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  4314  disjxun  5084  elidinxp  6003  cnvresima  6188  ordpwsuc  7759  supmo  9358  infmo  9403  kmlem3  10066  cfval2  10173  eqger  19144  gaorber  19274  opprunit  20348  issubrng  20515  xmeter  24408  iscvsp  25105  elold  27865  usgr2pth0  29848  axregs  35299  mh-infprim2bi  36745  mh-infprim3bi  36746  bj-dfnnf2  37052  funALTVfun  39118  clsk1indlem4  44489  alimp-no-surprise  50268