Theorem anbi2ci 627

Description: Variant of anbi2i 625 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 626	. 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  1070  clabel  2934  difin0ss  4282  disjxun  5028  elidinxp  5878  cnvresima  6054  ordpwsuc  7510  supmo  8900  infmo  8943  kmlem3  9563  cfval2  9671  eqger  18322  gaorber  18430  opprunit  19407  xmeter  23040  iscvsp  23733  usgr2pth0  27554  bj-dfnnf2  34181  funALTVfun  36091  clsk1indlem4  40747  alimp-no-surprise  45309