Theorem anbi12ci 629

Description: Variant of anbi12i 628 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 628	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
4	3	biancomi 462	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜃 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  eu1  2603  compleq  4111  cnvpo  6248  f1cnvcnv  6747  fsplit  8073  cnvimadfsn  8128  oppcsect  17720  oduprs  18241  odupos  18267  oppr1  20270  ordtrest2  23124  wwlks2onsym  29938  3cyclfrgrrn1  30264  fusgr2wsp2nb  30313  mdsldmd1i  32310  isunit2  33207  ordtrest2NEW  33906  cnvco1  35739  cnvco2  35740  pocnv  35743  dfiota3  35904  brcup  35920  brcap  35921  trer  36297  bj-nnfnt  36721  bj-gabima  36921  undmrnresiss  43586  dffrege115  43960  pgnbgreunbgrlem1  48096  pgnbgreunbgrlem4  48102