Theorem an4 586

Description: Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)

Assertion

Ref	Expression
an4	⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Proof of Theorem an4

Step	Hyp	Ref	Expression
1		an12 561	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
2	1	anbi2i 457	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃))))
3		anass 401	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
4		anass 401	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃))))
5	2, 3, 4	3bitr4i 212	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Syntax hints:   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an42  587  an4s  588  anandi  590  anandir  591  rnlem  976  an6  1321  2eu4  2119  reean  2646  reu2  2926  rmo4  2931  rmo3f  2935  rmo3  3055  inxp  4762  xp11m  5068  fununi  5285  fun  5389  resoprab2  5972  xporderlem  6232  poxp  6233  th3qlem1  6637  enq0enq  7430  enq0tr  7433  genpdisj  7522  cju  8918  elfzo2  10150  iooinsup  11285  summodc  11391  prodmodc  11586  issubmd  12865  dvdsrtr  13270  txbasval  13770  txcnp  13774  txlm  13782