Theorem anbi2ci 631

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

Syntax hints:   ↔ wb 207   ∧ wa 396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  clabel  2885  difin0ss  4308  disjxun  5077  elidinxp  6003  cnvresima  6188  ordpwsuc  7762  supmo  9362  infmo  9407  kmlem3  10073  cfval2  10180  eqger  19151  gaorber  19281  opprunit  20355  issubrng  20526  xmeter  24423  iscvsp  25120  elold  27876  usgr2pth0  29858  axregs  35327  mh-infprim2bi  36782  mh-infprim3bi  36783  bj-dfnnf2  37089  funALTVfun  39157  clsk1indlem4  44495  alimp-no-surprise  50278