Theorem anbi12ci 637

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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  eu1  2631  compleq  4100  cnvpo  6263  f1cnvcnv  6760  fsplit  8084  cnvimadfsn  8140  oppcsect  17787  oduprs  18308  odupos  18334  oppr1  20371  ordtrest2  23237  wwlks2onsym  30099  3cyclfrgrrn1  30426  fusgr2wsp2nb  30475  mdsldmd1i  32473  isunit2  33374  ordtrest2NEW  34174  cnvco1  36057  cnvco2  36058  pocnv  36061  dfiota3  36219  brcup  36235  brcap  36236  trer  36624  mh-infprim1bi  36854  bj-nnfnt  37173  bj-gabima  37373  undmrnresiss  44128  dffrege115  44502  pgnbgreunbgrlem1  48683  pgnbgreunbgrlem4  48689