Theorem an4 592

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 567	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
2	1	anbi2i 461	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃))))
3		anass 405	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
4		anass 405	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃))))
5	2, 3, 4	3bitr4i 212	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  an42  593  an4s  596  anandi  598  anandir  599  rnlem  989  an6  1362  2eu4  2180  reean  2720  reu2  3014  rmo4  3019  rmo3f  3023  rmo3  3144  inxp  4914  xp11m  5226  fununi  5449  fun  5561  resoprab2  6185  xporderlem  6467  poxp  6468  th3qlem1  6911  enq0enq  7798  enq0tr  7801  genpdisj  7890  cju  9293  elfzo2  10567  iooinsup  12059  summodc  12166  prodmodc  12361  issubmd  13830  dvdsrtr  14457  domnmuln0  14631  txbasval  15417  txcnp  15421  txlm  15429