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  2603  compleq  4115  cnvpo  6260  f1cnvcnv  6765  fsplit  8096  cnvimadfsn  8151  oppcsect  17740  oduprs  18261  odupos  18287  oppr1  20259  ordtrest2  23091  wwlks2onsym  29888  3cyclfrgrrn1  30214  fusgr2wsp2nb  30263  mdsldmd1i  32260  isunit2  33191  ordtrest2NEW  33913  cnvco1  35746  cnvco2  35747  pocnv  35750  dfiota3  35911  brcup  35927  brcap  35928  trer  36304  bj-nnfnt  36728  bj-gabima  36928  undmrnresiss  43593  dffrege115  43967  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem4  48109