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  2605  compleq  4099  cnvpo  6234  f1cnvcnv  6728  fsplit  8047  cnvimadfsn  8102  oppcsect  17685  oduprs  18206  odupos  18232  oppr1  20268  ordtrest2  23119  wwlks2onsym  29938  3cyclfrgrrn1  30265  fusgr2wsp2nb  30314  mdsldmd1i  32311  isunit2  33207  ordtrest2NEW  33936  cnvco1  35803  cnvco2  35804  pocnv  35807  dfiota3  35965  brcup  35981  brcap  35982  trer  36360  bj-nnfnt  36784  bj-gabima  36984  undmrnresiss  43707  dffrege115  44081  pgnbgreunbgrlem1  48223  pgnbgreunbgrlem4  48229