Theorem anbi2ci 637

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  clabel  2911  difin0ss  4331  disjxun  5112  elidinxp  6051  cnvresima  6236  ordpwsuc  7820  supmo  9422  infmo  9467  kmlem3  10155  cfval2  10262  eqger  19277  gaorber  19409  opprunit  20492  issubrng  20683  xmeter  24627  iscvsp  25324  elold  28089  usgr2pth0  30151  axregs  35576  mh-infprim2bi  37099  mh-infprim3bi  37100  bj-dfnnf2  37405  funALTVfun  39473  clsk1indlem4  44811  alimp-no-surprise  50600