Theorem anbi2ci 619

Description: Variant of anbi2i 617 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 618	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
3		ancom 453	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
4	2, 3	bitri 267	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 198   ∧ wa 385

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 199  df-an 386

This theorem is referenced by:  ifpn  1096  clabel  2924  difin0ss  4145  disjxun  4839  elidinxp  5665  cnvresima  5840  ordpwsuc  7247  supmo  8598  infmo  8641  kmlem3  9260  cfval2  9368  eqger  17953  gaorber  18049  opprunit  18973  xmeter  22562  iscvsp  23251  usgr2pth0  27010  bj-clabel  33270  clsk1indlem4  39111  alimp-no-surprise  43316