Theorem anbi12ci 730

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

Syntax hints:   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  eu1  2498  compleq  3714  opelopabsbALT  4909  cnvpo  5590  f1cnvcnv  6022  cnvimadfsn  7191  oppcsect  16261  odupos  16958  oppr1  18457  ordtrest2  20818  3cyclfrgrarn1  26539  mdsldmd1i  28574  oduprs  28987  ordtrest2NEW  29297  cnvco1  30903  cnvco2  30904  pocnv  30907  dfiota3  31200  brcup  31216  brcap  31217  dfrdg4  31228  trer  31480  bj-ssbequ2  31832  dffrege115  37292  3cyclfrgrrn1  41455  frgr2wwlkeqm  41496