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  13an22anass  1379  an6  1474  reeanlem  3234  reu2  3683  rmo4  3688  rmo3f  3692  rmo3  3836  2reu1  3845  2reu4lem  4479  disjiun  5091  inxp  5809  xp11  6167  dfpo2  6298  fununi  6613  fun  6742  resoprab2  7537  sorpsscmpl  7748  xporderlem  8137  poxp  8138  poseq  8168  fprlem1  8311  frrlem15  9754  dfac5lem1  10195  zorn2lem6  10572  cju  12309  ixxin  13486  elfzo2  13789  xpcogend  15120  summo  15876  prodmo  16096  dfiso2  17940  issubmd  18994  gsumval3eu  20111  dvdsrtr  20591  isirred2  20644  domnmuln0  20954  isdomn3  20959  abvn0b  21086  lspsolvlem  21413  unocv  21979  pf1ind  22666  ordtrest2lem  23514  lmmo  23691  ptbasin  23889  txbasval  23918  txcnp  23932  txlm  23960  tx1stc  23962  tx2ndc  23963  isfild  24170  txflf  24318  isclmp  25411  mbfi1flimlem  26036  iblcnlem1  26101  iblre  26107  iblcn  26112  logfaclbnd  27542  ons2ind  28654  axcontlem4  29538  axcontlem7  29541  ocsh  31878  pjhthmo  31897  5oalem6  32254  cvnbtwn4  32884  superpos  32949  cdj3i  33036  smatrcl  34421  ordtrest2NEWlem  34547  cusgr3cyclex  35890  lineext  36821  outsideoftr  36874  hilbert1.2  36900  lineintmo  36902  neibastop1  37127  bj-inrab  37820  isbasisrelowllem1  38258  isbasisrelowllem2  38259  ptrest  38517  poimirlem26  38544  ismblfin  38559  unirep  38628  inixp  38642  ablo4pnp  38794  keridl  38946  ispridlc  38984  anan  39147  disjecxrn  39324  coss1cnvres  39419  br1cosscnvxrn  39476  dfeldisj3  39723  antisymrelres  39778  prtlem70  39894  lcvbr3  40060  cvrnbtwn4  40316  linepsubN  40789  pmapsub  40805  pmapjoin  40889  ltrnu  41158  diblsmopel  42208  pell1234qrmulcl  43841  ifpan23  44445  ifpidg  44476  ifpbibib  44495  uneqsn  45010  isthincd2  50514