Theorem anbi12ci 641

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  eu1  2636  compleq  4099  cnvpo  6290  f1cnvcnv  6789  fsplit  8128  cnvimadfsn  8189  oppcsect  17953  oduprs  18474  odupos  18500  oppr1  20580  ordtrest2  23522  wwlks2onsym  30549  3cyclfrgrrn1  30886  fusgr2wsp2nb  30935  mdsldmd1i  32933  isunit2  33800  ordtrest2NEW  34555  cnvco1  36524  cnvco2  36525  pocnv  36528  dfiota3  36685  brcup  36701  brcap  36702  trer  37104  mh-infprim1bi  37334  bj-nnfnt  37652  bj-gabima  37853  undmrnresiss  44603  dffrege115  44977  pgnbgreunbgrlem1  49210  pgnbgreunbgrlem4  49216