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  1071  clabel  2884  difin0ss  4299  disjxun  5068  elidinxp  5940  cnvresima  6122  ordpwsuc  7637  supmo  9141  infmo  9184  kmlem3  9839  cfval2  9947  eqger  18721  gaorber  18829  opprunit  19818  xmeter  23494  iscvsp  24197  usgr2pth0  28034  elold  33980  bj-dfnnf2  34846  funALTVfun  36736  clsk1indlem4  41543  alimp-no-surprise  46371