Theorem anbi12ci 627

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

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  eu1  2613  compleq  4086  cnvpo  6187  f1cnvcnv  6676  fsplit  7941  fsplitOLD  7942  cnvimadfsn  7972  oppcsect  17471  odupos  18027  oppr1  19857  ordtrest2  22336  wwlks2onsym  28302  3cyclfrgrrn1  28628  fusgr2wsp2nb  28677  mdsldmd1i  30672  oduprs  31221  ordtrest2NEW  31852  cnvco1  33705  cnvco2  33706  pocnv  33709  dfiota3  34204  brcup  34220  brcap  34221  trer  34484  bj-nnfnt  34901  bj-gabima  35107  undmrnresiss  41165  dffrege115  41539