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  2644  compleq  4114  cnvpo  6289  f1cnvcnv  6786  fsplit  8112  cnvimadfsn  8168  oppcsect  17835  oduprs  18356  odupos  18382  oppr1  20432  ordtrest2  23330  wwlks2onsym  30250  3cyclfrgrrn1  30577  fusgr2wsp2nb  30626  mdsldmd1i  32624  isunit2  33500  ordtrest2NEW  34258  cnvco1  36184  cnvco2  36185  pocnv  36188  dfiota3  36346  brcup  36362  brcap  36363  trer  36750  mh-infprim1bi  36980  bj-nnfnt  37298  bj-gabima  37498  undmrnresiss  44256  dffrege115  44630  pgnbgreunbgrlem1  48801  pgnbgreunbgrlem4  48807