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 462	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜃 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  eu1  2609  compleq  4151  cnvpo  6306  f1cnvcnv  6812  fsplit  8143  cnvimadfsn  8198  oppcsect  17823  oduprs  18347  odupos  18374  oppr1  20351  ordtrest2  23213  wwlks2onsym  29979  3cyclfrgrrn1  30305  fusgr2wsp2nb  30354  mdsldmd1i  32351  isunit2  33245  ordtrest2NEW  33923  cnvco1  35760  cnvco2  35761  pocnv  35764  dfiota3  35925  brcup  35941  brcap  35942  trer  36318  bj-nnfnt  36742  bj-gabima  36942  undmrnresiss  43622  dffrege115  43996