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  2906  difin0ss  4321  disjxun  5101  elidinxp  6038  cnvresima  6224  ordpwsuc  7815  supmo  9428  infmo  9473  kmlem3  10212  cfval2  10319  eqger  19370  gaorber  19502  opprunit  20587  issubrng  20779  xmeter  24732  iscvsp  25429  elold  28227  usgr2pth0  30333  axregs  35780  mh-infprim2bi  37305  mh-infprim3bi  37306  bj-dfnnf2  37611  funALTVfun  39683  clsk1indlem4  45003  alimp-no-surprise  50821