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  2878  difin0ss  4322  disjxun  5091  elidinxp  5997  cnvresima  6182  ordpwsuc  7751  supmo  9343  infmo  9388  kmlem3  10051  cfval2  10158  eqger  19092  gaorber  19222  opprunit  20297  issubrng  20464  xmeter  24349  iscvsp  25056  elold  27815  usgr2pth0  29745  axregs  35166  bj-dfnnf2  36802  funALTVfun  38817  clsk1indlem4  44162  alimp-no-surprise  49907