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  2638  compleq  4091  cnvpo  6297  f1cnvcnv  6800  fsplit  8141  cnvimadfsn  8203  oppcsect  17968  oduprs  18489  odupos  18515  oppr1  20595  ordtrest2  23537  wwlks2onsym  30564  3cyclfrgrrn1  30901  fusgr2wsp2nb  30950  mdsldmd1i  32948  isunit2  33856  ordtrest2NEW  34611  cnvco1  36654  cnvco2  36655  pocnv  36658  dfiota3  36815  brcup  36831  brcap  36832  trer  37234  mh-infprim1bi  37464  bj-nnfnt  37782  bj-gabima  37983  undmrnresiss  44747  dffrege115  45121  pgnbgreunbgrlem1  49353  pgnbgreunbgrlem4  49359