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  2905  difin0ss  4320  disjxun  5100  elidinxp  6035  cnvresima  6231  ordpwsuc  7826  supmo  9447  infmo  9492  kmlem3  10234  cfval2  10341  eqger  19395  gaorber  19527  opprunit  20612  issubrng  20804  xmeter  24757  iscvsp  25454  elold  28250  usgr2pth0  30356  axregs  35863  mh-infprim2bi  37427  mh-infprim3bi  37428  bj-dfnnf2  37733  funALTVfun  39808  clsk1indlem4  45137  alimp-no-surprise  51045