Theorem anbi12ci 629

Description: Variant of anbi12i 628 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
anbi12.1	⊢ (𝜑 ↔ 𝜓)
anbi12.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
anbi12ci	⊢ ((𝜑 ∧ 𝜒) ↔ (𝜃 ∧ 𝜓))

Proof of Theorem anbi12ci

Step	Hyp	Ref	Expression
1		anbi12.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		anbi12.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	1, 2	anbi12i 628	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
4	3	biancomi 462	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜃 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  eu1  2610  compleq  4132  cnvpo  6281  f1cnvcnv  6788  fsplit  8121  cnvimadfsn  8176  oppcsect  17796  oduprs  18317  odupos  18343  oppr1  20315  ordtrest2  23147  wwlks2onsym  29945  3cyclfrgrrn1  30271  fusgr2wsp2nb  30320  mdsldmd1i  32317  isunit2  33240  ordtrest2NEW  33959  cnvco1  35781  cnvco2  35782  pocnv  35785  dfiota3  35946  brcup  35962  brcap  35963  trer  36339  bj-nnfnt  36763  bj-gabima  36963  undmrnresiss  43595  dffrege115  43969