Theorem an4 656

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  an42  657  an4s  660  anandi  676  anandir  677  an6  1447  reeanlem  3209  reu2  3699  rmo4  3704  rmo3f  3708  rmo3  3855  2reu1  3863  2reu4lem  4488  disjiun  5098  inxp  5798  inxpOLD  5799  xp11  6151  dfpo2  6272  fununi  6594  fun  6725  resoprab2  7511  sorpsscmpl  7713  xporderlem  8109  poxp  8110  poseq  8140  fprlem1  8282  frrlem15  9717  dfac5lem1  10083  zorn2lem6  10461  cju  12189  ixxin  13330  elfzo2  13630  xpcogend  14947  summo  15690  prodmo  15909  dfiso2  17741  issubmd  18740  gsumval3eu  19841  dvdsrtr  20284  isirred2  20337  domnmuln0  20625  isdomn3  20631  abvn0b  20752  lspsolvlem  21059  unocv  21596  pf1ind  22249  ordtrest2lem  23097  lmmo  23274  ptbasin  23471  txbasval  23500  txcnp  23514  txlm  23542  tx1stc  23544  tx2ndc  23545  isfild  23752  txflf  23900  isclmp  25004  mbfi1flimlem  25630  iblcnlem1  25696  iblre  25702  iblcn  25707  logfaclbnd  27140  axcontlem4  28901  axcontlem7  28904  ocsh  31219  pjhthmo  31238  5oalem6  31595  cvnbtwn4  32225  superpos  32290  cdj3i  32377  13an22anass  32400  smatrcl  33793  ordtrest2NEWlem  33919  cusgr3cyclex  35130  lineext  36071  outsideoftr  36124  hilbert1.2  36150  lineintmo  36152  neibastop1  36354  bj-inrab  36922  isbasisrelowllem1  37350  isbasisrelowllem2  37351  ptrest  37620  poimirlem26  37647  ismblfin  37662  unirep  37715  inixp  37729  ablo4pnp  37881  keridl  38033  ispridlc  38071  anan  38224  disjecxrn  38382  coss1cnvres  38415  br1cosscnvxrn  38472  dfeldisj3  38718  antisymrelres  38762  prtlem70  38857  lcvbr3  39023  cvrnbtwn4  39279  linepsubN  39753  pmapsub  39769  pmapjoin  39853  ltrnu  40122  diblsmopel  41172  pell1234qrmulcl  42850  ifpan23  43456  ifpidg  43487  ifpbibib  43506  uneqsn  44021  isthincd2  49430