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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  eu1  2694  compleq  4124  opelopabsbALT  5416  cnvpo  6138  f1cnvcnv  6584  fsplit  7812  fsplitOLD  7813  cnvimadfsn  7839  oppcsect  17048  odupos  17745  oppr1  19384  ordtrest2  21812  wwlks2onsym  27737  3cyclfrgrrn1  28064  fusgr2wsp2nb  28113  mdsldmd1i  30108  oduprs  30643  ordtrest2NEW  31166  cnvco1  32995  cnvco2  32996  pocnv  32999  dfiota3  33384  brcup  33400  brcap  33401  trer  33664  bj-nnfnt  34069  undmrnresiss  39984  dffrege115  40344