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 464	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜃 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  eu1  2610  compleq  4088  cnvpo  6205  f1cnvcnv  6710  fsplit  7989  cnvimadfsn  8019  oppcsect  17539  odupos  18095  oppr1  19925  ordtrest2  22404  wwlks2onsym  28372  3cyclfrgrrn1  28698  fusgr2wsp2nb  28747  mdsldmd1i  30742  oduprs  31291  ordtrest2NEW  31922  cnvco1  33775  cnvco2  33776  pocnv  33779  dfiota3  34274  brcup  34290  brcap  34291  trer  34554  bj-nnfnt  34971  bj-gabima  35176  undmrnresiss  41425  dffrege115  41799