Theorem anbi12ci 631

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

Syntax hints:   ↔ wb 209   ∧ wa 399

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 400

This theorem is referenced by:  eu1  2613  compleq  4038  cnvpo  6119  f1cnvcnv  6584  fsplit  7838  fsplitOLD  7839  cnvimadfsn  7867  oppcsect  17153  odupos  17861  oppr1  19506  ordtrest2  21955  wwlks2onsym  27896  3cyclfrgrrn1  28222  fusgr2wsp2nb  28271  mdsldmd1i  30266  oduprs  30816  ordtrest2NEW  31445  cnvco1  33298  cnvco2  33299  pocnv  33302  dfiota3  33863  brcup  33879  brcap  33880  trer  34143  bj-nnfnt  34560  undmrnresiss  40757  dffrege115  41132