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  2910  difin0ss  4329  disjxun  5103  elidinxp  6037  cnvresima  6221  ordpwsuc  7799  supmo  9400  infmo  9445  kmlem3  10124  cfval2  10232  eqger  19237  gaorber  19369  opprunit  20450  issubrng  20623  xmeter  24551  iscvsp  25248  elold  28010  usgr2pth0  30023  axregs  35447  mh-infprim2bi  36920  mh-infprim3bi  36921  bj-dfnnf2  37226  funALTVfun  39294  clsk1indlem4  44632  alimp-no-surprise  50410