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  2693  compleq  4127  opelopabsbALT  5419  cnvpo  6141  f1cnvcnv  6587  fsplit  7815  fsplitOLD  7816  cnvimadfsn  7842  oppcsect  17051  odupos  17748  oppr1  19387  ordtrest2  21815  wwlks2onsym  27740  3cyclfrgrrn1  28067  fusgr2wsp2nb  28116  mdsldmd1i  30111  oduprs  30647  ordtrest2NEW  31170  cnvco1  32999  cnvco2  33000  pocnv  33003  dfiota3  33388  brcup  33404  brcap  33405  trer  33668  bj-nnfnt  34073  undmrnresiss  39970  dffrege115  40330