Theorem anbi12ci 622

Description: Variant of anbi12i 621 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 621	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
4		ancom 453	. 2 ⊢ ((𝜓 ∧ 𝜃) ↔ (𝜃 ∧ 𝜓))
5	3, 4	bitri 267	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜃 ∧ 𝜓))

Syntax hints:   ↔ wb 198   ∧ wa 385

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 199  df-an 386

This theorem is referenced by:  eu1  2662  compleq  3950  opelopabsbALT  5180  cnvpo  5892  f1cnvcnv  6325  fsplit  7519  cnvimadfsn  7541  oppcsect  16752  odupos  17450  oppr1  18950  ordtrest2  21337  wwlks2onsym  27248  3cyclfrgrrn1  27634  fusgr2wsp2nb  27683  mdsldmd1i  29715  oduprs  30172  ordtrest2NEW  30485  cnvco1  32163  cnvco2  32164  pocnv  32167  dfiota3  32543  brcup  32559  brcap  32560  trer  32823  bj-ssbequ2  33149  undmrnresiss  38693  dffrege115  39054