Theorem anbi12ci 630

Description: Variant of anbi12i 629 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 629	. 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  2610  compleq  4092  cnvpo  6251  f1cnvcnv  6745  fsplit  8067  cnvimadfsn  8122  oppcsect  17745  oduprs  18266  odupos  18292  oppr1  20330  ordtrest2  23169  wwlks2onsym  30028  3cyclfrgrrn1  30355  fusgr2wsp2nb  30404  mdsldmd1i  32402  isunit2  33301  ordtrest2NEW  34067  cnvco1  35941  cnvco2  35942  pocnv  35945  dfiota3  36103  brcup  36119  brcap  36120  trer  36498  mh-infprim1bi  36728  bj-nnfnt  37047  bj-gabima  37247  undmrnresiss  44031  dffrege115  44405  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem4  48595