Theorem anbi12ci 627

Description: Variant of anbi12i 626 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 626	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
4	3	biancomi 462	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜃 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  eu1  2601  compleq  4143  cnvpo  6285  f1cnvcnv  6797  fsplit  8116  cnvimadfsn  8170  oppcsect  17752  odupos  18311  oppr1  20278  ordtrest2  23095  wwlks2onsym  29756  3cyclfrgrrn1  30082  fusgr2wsp2nb  30131  mdsldmd1i  32128  oduprs  32673  ordtrest2NEW  33460  cnvco1  35289  cnvco2  35290  pocnv  35293  dfiota3  35455  brcup  35471  brcap  35472  trer  35736  bj-nnfnt  36153  bj-gabima  36354  undmrnresiss  42957  dffrege115  43331