Theorem anbi2ci 636

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 401

This theorem is referenced by:  clabel  2908  difin0ss  4329  disjxun  5108  elidinxp  6048  cnvresima  6233  ordpwsuc  7812  supmo  9413  infmo  9458  kmlem3  10137  cfval2  10245  eqger  19247  gaorber  19379  opprunit  20460  issubrng  20633  xmeter  24571  iscvsp  25268  elold  28030  usgr2pth0  30092  axregs  35530  mh-infprim2bi  37036  mh-infprim3bi  37037  bj-dfnnf2  37342  funALTVfun  39410  clsk1indlem4  44750  alimp-no-surprise  50536