Theorem an4 668

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 473	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
2		an12 657	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
3	2	bianass 654	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))
4	1, 3	bitri 278	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  an42  669  an4s  672  anandi  688  anandir  689  13an22anass  1379  an6  1474  reeanlem  3236  reu2  3689  rmo4  3694  rmo3f  3698  rmo3  3843  2reu1  3852  2reu4lem  4485  disjiun  5098  inxp  5820  xp11  6175  dfpo2  6299  fununi  6613  fun  6742  resoprab2  7531  sorpsscmpl  7733  xporderlem  8124  poxp  8125  poseq  8155  fprlem1  8298  frrlem15  9730  dfac5lem1  10108  zorn2lem6  10486  cju  12215  ixxin  13390  elfzo2  13692  xpcogend  15013  summo  15770  prodmo  15992  dfiso2  17830  issubmd  18865  gsumval3eu  19975  dvdsrtr  20451  isirred2  20504  domnmuln0  20795  isdomn3  20800  abvn0b  20920  lspsolvlem  21247  unocv  21811  pf1ind  22496  ordtrest2lem  23341  lmmo  23518  ptbasin  23715  txbasval  23744  txcnp  23758  txlm  23786  tx1stc  23788  tx2ndc  23789  isfild  23996  txflf  24144  isclmp  25237  mbfi1flimlem  25862  iblcnlem1  25928  iblre  25934  iblcn  25939  logfaclbnd  27367  ons2ind  28449  axcontlem4  29298  axcontlem7  29301  ocsh  31616  pjhthmo  31635  5oalem6  31992  cvnbtwn4  32622  superpos  32687  cdj3i  32774  smatrcl  34167  ordtrest2NEWlem  34293  cusgr3cyclex  35609  lineext  36549  outsideoftr  36602  hilbert1.2  36628  lineintmo  36630  neibastop1  36851  bj-inrab  37544  isbasisrelowllem1  37982  isbasisrelowllem2  37983  ptrest  38251  poimirlem26  38278  ismblfin  38293  unirep  38346  inixp  38360  ablo4pnp  38512  keridl  38664  ispridlc  38702  anan  38865  disjecxrn  39042  coss1cnvres  39137  br1cosscnvxrn  39194  dfeldisj3  39441  antisymrelres  39496  prtlem70  39612  lcvbr3  39778  cvrnbtwn4  40034  linepsubN  40507  pmapsub  40523  pmapjoin  40607  ltrnu  40876  diblsmopel  41926  pell1234qrmulcl  43565  ifpan23  44169  ifpidg  44200  ifpbibib  44219  uneqsn  44734  isthincd2  50198