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  2907  difin0ss  4324  disjxun  5105  elidinxp  6044  cnvresima  6230  ordpwsuc  7815  supmo  9426  infmo  9471  kmlem3  10159  cfval2  10266  eqger  19309  gaorber  19441  opprunit  20524  issubrng  20715  xmeter  24665  iscvsp  25362  elold  28132  usgr2pth0  30238  axregs  35673  mh-infprim2bi  37174  mh-infprim3bi  37175  bj-dfnnf2  37480  funALTVfun  39539  clsk1indlem4  44892  alimp-no-surprise  50718