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  2611  compleq  4106  cnvpo  6253  f1cnvcnv  6747  fsplit  8069  cnvimadfsn  8124  oppcsect  17714  oduprs  18235  odupos  18261  oppr1  20298  ordtrest2  23160  wwlks2onsym  30045  3cyclfrgrrn1  30372  fusgr2wsp2nb  30421  mdsldmd1i  32419  isunit2  33334  ordtrest2NEW  34101  cnvco1  35975  cnvco2  35976  pocnv  35979  dfiota3  36137  brcup  36153  brcap  36154  trer  36532  bj-nnfnt  36993  bj-gabima  37188  undmrnresiss  43960  dffrege115  44334  pgnbgreunbgrlem1  48473  pgnbgreunbgrlem4  48479