Theorem anbi12ci 630

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

Syntax hints:   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  eu1  2671  compleq  4075  opelopabsbALT  5381  cnvpo  6106  f1cnvcnv  6559  fsplit  7795  fsplitOLD  7796  cnvimadfsn  7822  oppcsect  17040  odupos  17737  oppr1  19380  ordtrest2  21809  wwlks2onsym  27744  3cyclfrgrrn1  28070  fusgr2wsp2nb  28119  mdsldmd1i  30114  oduprs  30669  ordtrest2NEW  31276  cnvco1  33108  cnvco2  33109  pocnv  33112  dfiota3  33497  brcup  33513  brcap  33514  trer  33777  bj-nnfnt  34184  undmrnresiss  40304  dffrege115  40679