Theorem anbi2ci 624

Description: Variant of anbi2i 622 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 623	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
3	2	biancomi 462	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  ifpnOLD  1072  clabel  2880  difin0ss  4368  disjxun  5146  elidinxp  6043  cnvresima  6229  ordpwsuc  7807  supmo  9453  infmo  9496  kmlem3  10153  cfval2  10261  eqger  19101  gaorber  19220  opprunit  20275  issubrng  20443  xmeter  24259  iscvsp  24975  elold  27710  usgr2pth0  29456  bj-dfnnf2  36081  funALTVfun  38034  clsk1indlem4  43260  alimp-no-surprise  47992