Theorem anbi12ci 734

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

Syntax hints:   ↔ wb 196   ∧ wa 384

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

This theorem is referenced by:  eu1  2510  compleq  3752  opelopabsbALT  4984  cnvpo  5673  f1cnvcnv  6109  cnvimadfsn  7304  oppcsect  16438  odupos  17135  oppr1  18634  ordtrest2  21008  wwlks2onsym  26851  3cyclfrgrrn1  27149  fusgr2wsp2nb  27198  mdsldmd1i  29190  oduprs  29656  ordtrest2NEW  29969  cnvco1  31649  cnvco2  31650  pocnv  31653  dfiota3  32030  brcup  32046  brcap  32047  dfrdg4  32058  trer  32310  bj-ssbequ2  32643  dffrege115  38272