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 464	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  ifpnOLD  1074  clabel  2882  difin0ss  4369  disjxun  5147  elidinxp  6044  cnvresima  6230  ordpwsuc  7803  supmo  9447  infmo  9490  kmlem3  10147  cfval2  10255  eqger  19058  gaorber  19172  opprunit  20191  xmeter  23939  iscvsp  24644  elold  27364  usgr2pth0  29022  bj-dfnnf2  35615  funALTVfun  37568  clsk1indlem4  42795  issubrng  46726  alimp-no-surprise  47828