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  2603  compleq  4103  cnvpo  6235  f1cnvcnv  6729  fsplit  8050  cnvimadfsn  8105  oppcsect  17685  oduprs  18206  odupos  18232  oppr1  20235  ordtrest2  23089  wwlks2onsym  29903  3cyclfrgrrn1  30229  fusgr2wsp2nb  30278  mdsldmd1i  32275  isunit2  33180  ordtrest2NEW  33890  cnvco1  35736  cnvco2  35737  pocnv  35740  dfiota3  35901  brcup  35917  brcap  35918  trer  36294  bj-nnfnt  36718  bj-gabima  36918  undmrnresiss  43581  dffrege115  43955  pgnbgreunbgrlem1  48101  pgnbgreunbgrlem4  48107