Theorem anbi2ci 628

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

Syntax hints:   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ifpnOLD  1075  clabel  2882  difin0ss  4283  disjxun  5051  elidinxp  5911  cnvresima  6093  ordpwsuc  7594  supmo  9068  infmo  9111  kmlem3  9766  cfval2  9874  eqger  18594  gaorber  18702  opprunit  19679  xmeter  23331  iscvsp  24025  usgr2pth0  27852  elold  33790  bj-dfnnf2  34656  funALTVfun  36546  clsk1indlem4  41331  alimp-no-surprise  46156