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  2909  difin0ss  4324  disjxun  5104  elidinxp  6048  cnvresima  6244  ordpwsuc  7850  supmo  9471  infmo  9516  kmlem3  10258  cfval2  10365  eqger  19419  gaorber  19552  opprunit  20637  issubrng  20829  xmeter  24782  iscvsp  25479  elold  28275  usgr2pth0  30381  axregs  35907  mh-infprim2bi  37513  mh-infprim3bi  37514  bj-dfnnf2  37819  funALTVfun  39907  clsk1indlem4  45236  alimp-no-surprise  51157