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  2610  compleq  4104  cnvpo  6245  f1cnvcnv  6739  fsplit  8059  cnvimadfsn  8114  oppcsect  17702  oduprs  18223  odupos  18249  oppr1  20286  ordtrest2  23148  wwlks2onsym  30033  3cyclfrgrrn1  30360  fusgr2wsp2nb  30409  mdsldmd1i  32406  isunit2  33322  ordtrest2NEW  34080  cnvco1  35953  cnvco2  35954  pocnv  35957  dfiota3  36115  brcup  36131  brcap  36132  trer  36510  bj-nnfnt  36941  bj-gabima  37141  undmrnresiss  43855  dffrege115  44229  pgnbgreunbgrlem1  48369  pgnbgreunbgrlem4  48375