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  2640  compleq  4106  cnvpo  6292  f1cnvcnv  6789  fsplit  8118  cnvimadfsn  8174  oppcsect  17859  oduprs  18380  odupos  18406  oppr1  20480  ordtrest2  23413  wwlks2onsym  30378  3cyclfrgrrn1  30709  fusgr2wsp2nb  30758  mdsldmd1i  32756  isunit2  33625  ordtrest2NEW  34379  cnvco1  36290  cnvco2  36291  pocnv  36294  dfiota3  36452  brcup  36468  brcap  36469  trer  36886  mh-infprim1bi  37116  bj-nnfnt  37434  bj-gabima  37635  undmrnresiss  44390  dffrege115  44764  pgnbgreunbgrlem1  48938  pgnbgreunbgrlem4  48944