Theorem anbi12ci 628

Description: Variant of anbi12i 627 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 627	. 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  2613  compleq  4175  cnvpo  6318  f1cnvcnv  6826  fsplit  8158  cnvimadfsn  8213  oppcsect  17839  odupos  18398  oppr1  20376  ordtrest2  23233  wwlks2onsym  29991  3cyclfrgrrn1  30317  fusgr2wsp2nb  30366  mdsldmd1i  32363  oduprs  32937  isunit2  33220  ordtrest2NEW  33869  cnvco1  35721  cnvco2  35722  pocnv  35725  dfiota3  35887  brcup  35903  brcap  35904  trer  36282  bj-nnfnt  36706  bj-gabima  36906  undmrnresiss  43566  dffrege115  43940