Theorem anbi12ci 641

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  eu1  2635  compleq  4099  cnvpo  6285  f1cnvcnv  6783  fsplit  8115  cnvimadfsn  8171  oppcsect  17870  oduprs  18391  odupos  18417  oppr1  20494  ordtrest2  23432  wwlks2onsym  30431  3cyclfrgrrn1  30768  fusgr2wsp2nb  30817  mdsldmd1i  32815  isunit2  33682  ordtrest2NEW  34436  cnvco1  36341  cnvco2  36342  pocnv  36345  dfiota3  36503  brcup  36519  brcap  36520  trer  36938  mh-infprim1bi  37168  bj-nnfnt  37486  bj-gabima  37687  undmrnresiss  44447  dffrege115  44821  pgnbgreunbgrlem1  49032  pgnbgreunbgrlem4  49038