Theorem anbi12ci 629

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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  eu1  2607  compleq  4148  cnvpo  6287  f1cnvcnv  6798  fsplit  8103  cnvimadfsn  8157  oppcsect  17725  odupos  18281  oppr1  20164  ordtrest2  22708  wwlks2onsym  29212  3cyclfrgrrn1  29538  fusgr2wsp2nb  29587  mdsldmd1i  31584  oduprs  32134  ordtrest2NEW  32903  cnvco1  34729  cnvco2  34730  pocnv  34733  dfiota3  34895  brcup  34911  brcap  34912  trer  35201  bj-nnfnt  35618  bj-gabima  35820  undmrnresiss  42355  dffrege115  42729