Theorem anbi12ci 640

Description: Variant of anbi12i 639 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 639	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
4	3	biancomi 467	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜃 ∧ 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  eu1  2638  compleq  4106  cnvpo  6288  f1cnvcnv  6785  fsplit  8108  cnvimadfsn  8164  oppcsect  17830  oduprs  18351  odupos  18377  oppr1  20428  ordtrest2  23361  wwlks2onsym  30309  3cyclfrgrrn1  30636  fusgr2wsp2nb  30685  mdsldmd1i  32683  isunit2  33559  ordtrest2NEW  34313  cnvco1  36251  cnvco2  36252  pocnv  36255  dfiota3  36413  brcup  36429  brcap  36430  trer  36847  mh-infprim1bi  37077  bj-nnfnt  37395  bj-gabima  37596  undmrnresiss  44350  dffrege115  44724  pgnbgreunbgrlem1  48898  pgnbgreunbgrlem4  48904