Theorem anbi12ci 638

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

Syntax hints:   ↔ wb 208   ∧ wa 399

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 400

This theorem is referenced by:  eu1  2637  compleq  4105  cnvpo  6274  f1cnvcnv  6771  fsplit  8096  cnvimadfsn  8152  oppcsect  17811  oduprs  18332  odupos  18358  oppr1  20399  ordtrest2  23264  wwlks2onsym  30160  3cyclfrgrrn1  30487  fusgr2wsp2nb  30536  mdsldmd1i  32534  isunit2  33420  ordtrest2NEW  34220  cnvco1  36109  cnvco2  36110  pocnv  36113  dfiota3  36271  brcup  36287  brcap  36288  trer  36676  mh-infprim1bi  36906  bj-nnfnt  37225  bj-gabima  37425  undmrnresiss  44180  dffrege115  44554  pgnbgreunbgrlem1  48735  pgnbgreunbgrlem4  48741