Theorem an4 669

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

Assertion

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

Proof of Theorem an4

Step	Hyp	Ref	Expression
1		anass 474	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
2		an12 658	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
3	2	bianass 655	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))
4	1, 3	bitri 278	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an42  670  an4s  673  anandi  689  anandir  690  13an22anassOLD  1380  an6  1475  reeanlem  3237  reu2  3686  rmo4  3691  rmo3f  3695  rmo3  3840  2reu1  3849  2reu4lem  4482  disjiun  5096  inxp  5819  xp11  6185  dfpo2  6325  fununi  6645  fun  6774  resoprab2  7570  sorpsscmpl  7782  xporderlem  8176  poxp  8177  poseq  8212  fprlem1  8356  frrlem15  9798  dfac5lem1  10241  zorn2lem6  10618  cju  12356  ixxin  13533  elfzo2  13836  xpcogend  15170  summo  15927  prodmo  16147  dfiso2  17997  issubmd  19051  gsumval3eu  20169  dvdsrtr  20649  isirred2  20702  domnmuln0  21012  isdomn3  21017  abvn0b  21144  lspsolvlem  21471  unocv  22041  pf1ind  22728  ordtrest2lem  23576  lmmo  23753  ptbasin  23951  txbasval  23980  txcnp  23994  txlm  24022  tx1stc  24024  tx2ndc  24025  isfild  24232  txflf  24380  isclmp  25473  mbfi1flimlem  26098  iblcnlem1  26163  iblre  26169  iblcn  26174  logfaclbnd  27606  ons2ind  28718  axcontlem4  29602  axcontlem7  29605  ocsh  31942  pjhthmo  31961  5oalem6  32318  cvnbtwn4  32948  superpos  33013  cdj3i  33100  smatrcl  34539  ordtrest2NEWlem  34665  fwfffunres  35829  cusgr3cyclex  36109  lineext  37056  outsideoftr  37109  hilbert1.2  37135  lineintmo  37137  neibastop1  37362  bj-inrab  38055  bj-inxpALT  38176  isbasisrelowllem1  38546  isbasisrelowllem2  38547  ptrest  38805  poimirlem26  38832  ismblfin  38847  unirep  38916  inixp  38930  ablo4pnp  39080  keridl  39232  ispridlc  39270  anan  39433  disjecxrn  39610  coss1cnvres  39705  br1cosscnvxrn  39762  dfeldisj3  40009  antisymrelres  40064  prtlem70  40180  lcvbr3  40346  cvrnbtwn4  40602  linepsubN  41075  pmapsub  41091  pmapjoin  41175  ltrnu  41444  diblsmopel  42494  pell1234qrmulcl  44128  ifpan23  44722  ifpidg  44753  ifpbibib  44772  uneqsn  45286  isthincd2  50903