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  2608  compleq  4102  cnvpo  6243  f1cnvcnv  6737  fsplit  8057  cnvimadfsn  8112  oppcsect  17700  oduprs  18221  odupos  18247  oppr1  20284  ordtrest2  23146  wwlks2onsym  29982  3cyclfrgrrn1  30309  fusgr2wsp2nb  30358  mdsldmd1i  32355  isunit2  33271  ordtrest2NEW  34029  cnvco1  35902  cnvco2  35903  pocnv  35906  dfiota3  36064  brcup  36080  brcap  36081  trer  36459  bj-nnfnt  36884  bj-gabima  37084  undmrnresiss  43787  dffrege115  44161  pgnbgreunbgrlem1  48301  pgnbgreunbgrlem4  48307