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  2882  difin0ss  4353  disjxun  5122  elidinxp  6036  cnvresima  6224  ordpwsuc  7814  supmo  9469  infmo  9514  kmlem3  10172  cfval2  10279  eqger  19166  gaorber  19296  opprunit  20342  issubrng  20512  xmeter  24377  iscvsp  25084  elold  27838  usgr2pth0  29752  bj-dfnnf2  36760  funALTVfun  38721  clsk1indlem4  44035  alimp-no-surprise  49612