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  2604  compleq  4118  cnvpo  6263  f1cnvcnv  6768  fsplit  8099  cnvimadfsn  8154  oppcsect  17747  oduprs  18268  odupos  18294  oppr1  20266  ordtrest2  23098  wwlks2onsym  29895  3cyclfrgrrn1  30221  fusgr2wsp2nb  30270  mdsldmd1i  32267  isunit2  33198  ordtrest2NEW  33920  cnvco1  35753  cnvco2  35754  pocnv  35757  dfiota3  35918  brcup  35934  brcap  35935  trer  36311  bj-nnfnt  36735  bj-gabima  36935  undmrnresiss  43600  dffrege115  43974  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem4  48113