Theorem an4 588

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 563	. . 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  589  an4s  592  anandi  594  anandir  595  rnlem  984  an6  1357  2eu4  2173  reean  2702  reu2  2994  rmo4  2999  rmo3f  3003  rmo3  3124  inxp  4864  xp11m  5175  fununi  5398  fun  5508  resoprab2  6117  xporderlem  6395  poxp  6396  th3qlem1  6805  enq0enq  7650  enq0tr  7653  genpdisj  7742  cju  9140  elfzo2  10384  iooinsup  11837  summodc  11943  prodmodc  12138  issubmd  13556  dvdsrtr  14114  domnmuln0  14286  txbasval  14990  txcnp  14994  txlm  15002