Theorem anbi1ci 627

Description: Variant of anbi1i 625 with commutation. (Contributed by Peter Mazsa, 7-Mar-2020.)

Hypothesis

Ref	Expression
anbi.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
anbi1ci	⊢ ((𝜒 ∧ 𝜑) ↔ (𝜓 ∧ 𝜒))

Proof of Theorem anbi1ci

Step	Hyp	Ref	Expression
1		anbi.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	anbi2i 624	. 2 ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓))
3	2	biancomi 465	1 ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜓 ∧ 𝜒))

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  dfid3  5462  imai  5942  wfi  6181  dfac5lem3  9551  cf0  9673  coep  32987  frpoind  33080  brtxp  33341  sscoid  33374  brapply  33399  dfrdg4  33412  rnxrncnvepres  35663  rnxrnidres  35664  pmapglb  36921  polval2N  37057  rp-fakeoranass  39900  alephiso2  39937