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  4162  cnvpo  6309  f1cnvcnv  6814  fsplit  8141  cnvimadfsn  8196  oppcsect  17826  oduprs  18358  odupos  18386  oppr1  20367  ordtrest2  23228  wwlks2onsym  29988  3cyclfrgrrn1  30314  fusgr2wsp2nb  30363  mdsldmd1i  32360  isunit2  33230  ordtrest2NEW  33884  cnvco1  35739  cnvco2  35740  pocnv  35743  dfiota3  35905  brcup  35921  brcap  35922  trer  36299  bj-nnfnt  36723  bj-gabima  36923  undmrnresiss  43594  dffrege115  43968