Theorem anbi12ci 630

Description: Variant of anbi12i 629 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 629	. 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  2611  compleq  4093  cnvpo  6246  f1cnvcnv  6740  fsplit  8061  cnvimadfsn  8116  oppcsect  17739  oduprs  18260  odupos  18286  oppr1  20324  ordtrest2  23182  wwlks2onsym  30046  3cyclfrgrrn1  30373  fusgr2wsp2nb  30422  mdsldmd1i  32420  isunit2  33319  ordtrest2NEW  34086  cnvco1  35960  cnvco2  35961  pocnv  35964  dfiota3  36122  brcup  36138  brcap  36139  trer  36517  mh-infprim1bi  36747  bj-nnfnt  37066  bj-gabima  37266  undmrnresiss  44052  dffrege115  44426  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem4  48610