Theorem an4 655

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 470	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
2		an12 644	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
3	2	bianass 641	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))
4	1, 3	bitri 275	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Syntax hints:   ↔ wb 205   ∧ wa 397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  an42  656  an4s  659  anandi  675  anandir  676  an6  1446  an33reanOLD  1485  reeanlem  3226  reu2  3722  rmo4  3727  rmo3f  3731  rmo3  3884  2reu1  3892  2reu4lem  4526  disjiun  5136  inxp  5833  xp11  6175  dfpo2  6296  fununi  6624  fun  6754  resoprab2  7527  sorpsscmpl  7724  xporderlem  8113  poxp  8114  poseq  8144  fprlem1  8285  frrlem15  9752  dfac5lem1  10118  zorn2lem6  10496  cju  12208  ixxin  13341  elfzo2  13635  xpcogend  14921  summo  15663  prodmo  15880  dfiso2  17719  issubmd  18687  gsumval3eu  19772  dvdsrtr  20182  isirred2  20235  lspsolvlem  20755  domnmuln0  20914  abvn0b  20920  unocv  21233  pf1ind  21874  ordtrest2lem  22707  lmmo  22884  ptbasin  23081  txbasval  23110  txcnp  23124  txlm  23152  tx1stc  23154  tx2ndc  23155  isfild  23362  txflf  23510  isclmp  24613  mbfi1flimlem  25240  iblcnlem1  25305  iblre  25311  iblcn  25316  logfaclbnd  26725  axcontlem4  28225  axcontlem7  28228  ocsh  30536  pjhthmo  30555  5oalem6  30912  cvnbtwn4  31542  superpos  31607  cdj3i  31694  13an22anass  31706  smatrcl  32776  ordtrest2NEWlem  32902  cusgr3cyclex  34127  lineext  35048  outsideoftr  35101  hilbert1.2  35127  lineintmo  35129  neibastop1  35244  bj-inrab  35807  isbasisrelowllem1  36236  isbasisrelowllem2  36237  ptrest  36487  poimirlem26  36514  ismblfin  36529  unirep  36582  inixp  36596  ablo4pnp  36748  keridl  36900  ispridlc  36938  anan  37093  disjecxrn  37259  coss1cnvres  37287  br1cosscnvxrn  37344  dfeldisj3  37589  antisymrelres  37633  prtlem70  37727  lcvbr3  37893  cvrnbtwn4  38149  linepsubN  38623  pmapsub  38639  pmapjoin  38723  ltrnu  38992  diblsmopel  40042  pell1234qrmulcl  41593  isdomn3  41946  ifpan23  42211  ifpidg  42242  ifpbibib  42261  uneqsn  42776  isthincd2  47658