Theorem anbi12ci 635

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

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  eu1  2614  compleq  4082  cnvpo  6238  f1cnvcnv  6732  fsplit  8056  cnvimadfsn  8112  oppcsect  17736  oduprs  18257  odupos  18283  oppr1  20321  ordtrest2  23187  wwlks2onsym  30046  3cyclfrgrrn1  30373  fusgr2wsp2nb  30422  mdsldmd1i  32420  isunit2  33321  ordtrest2NEW  34107  cnvco1  35987  cnvco2  35988  pocnv  35991  dfiota3  36149  brcup  36165  brcap  36166  trer  36544  mh-infprim1bi  36774  bj-nnfnt  37093  bj-gabima  37293  undmrnresiss  44048  dffrege115  44422  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem4  48610