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  1377  an6  1471  reeanlem  3242  reu2  3697  rmo4  3702  rmo3f  3706  rmo3  3851  2reu1  3859  2reu4lem  4486  disjiun  5098  inxp  5816  xp11  6172  dfpo2  6294  fununi  6608  fun  6738  resoprab2  7527  sorpsscmpl  7729  xporderlem  8119  poxp  8120  poseq  8150  fprlem1  8293  frrlem15  9725  dfac5lem1  10103  zorn2lem6  10481  cju  12210  ixxin  13385  elfzo2  13686  xpcogend  15007  summo  15764  prodmo  15986  dfiso2  17825  issubmd  18860  gsumval3eu  19970  dvdsrtr  20446  isirred2  20499  domnmuln0  20790  isdomn3  20795  abvn0b  20913  lspsolvlem  21240  unocv  21795  pf1ind  22480  ordtrest2lem  23325  lmmo  23502  ptbasin  23699  txbasval  23728  txcnp  23742  txlm  23770  tx1stc  23772  tx2ndc  23773  isfild  23980  txflf  24128  isclmp  25221  mbfi1flimlem  25846  iblcnlem1  25912  iblre  25918  iblcn  25923  logfaclbnd  27348  ons2ind  28430  axcontlem4  29254  axcontlem7  29257  ocsh  31572  pjhthmo  31591  5oalem6  31948  cvnbtwn4  32578  superpos  32643  cdj3i  32730  smatrcl  34127  ordtrest2NEWlem  34253  cusgr3cyclex  35523  lineext  36463  outsideoftr  36516  hilbert1.2  36542  lineintmo  36544  neibastop1  36755  bj-inrab  37447  isbasisrelowllem1  37884  isbasisrelowllem2  37885  ptrest  38153  poimirlem26  38180  ismblfin  38195  unirep  38248  inixp  38262  ablo4pnp  38414  keridl  38566  ispridlc  38604  anan  38769  disjecxrn  38946  coss1cnvres  39041  br1cosscnvxrn  39098  dfeldisj3  39345  antisymrelres  39400  prtlem70  39516  lcvbr3  39682  cvrnbtwn4  39938  linepsubN  40411  pmapsub  40427  pmapjoin  40511  ltrnu  40780  diblsmopel  41830  pell1234qrmulcl  43467  ifpan23  44071  ifpidg  44102  ifpbibib  44121  uneqsn  44636  isthincd2  50093