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 465	. 2 ⊢ ((𝜓 ∧ 𝜃) ↔ (𝜃 ∧ 𝜓))
5	3, 4	bitri 264	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜃 ∧ 𝜓))

Syntax hints:   ↔ wb 196   ∧ 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 197  df-an 385

This theorem is referenced by:  eu1  2539  compleq  3785  opelopabsbALT  5013  cnvpo  5711  f1cnvcnv  6147  cnvimadfsn  7349  oppcsect  16485  odupos  17182  oppr1  18680  ordtrest2  21056  wwlks2onsym  26924  3cyclfrgrrn1  27265  fusgr2wsp2nb  27314  mdsldmd1i  29318  oduprs  29784  ordtrest2NEW  30097  cnvco1  31775  cnvco2  31776  pocnv  31779  dfiota3  32155  brcup  32171  brcap  32172  dfrdg4  32183  trer  32435  bj-ssbequ2  32768  dffrege115  38589