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  3212  reu2  3708  rmo4  3713  rmo3f  3717  rmo3  3864  2reu1  3872  2reu4lem  4497  disjiun  5107  inxp  5811  inxpOLD  5812  xp11  6164  dfpo2  6285  fununi  6611  fun  6740  resoprab2  7526  sorpsscmpl  7728  xporderlem  8126  poxp  8127  poseq  8157  fprlem1  8299  frrlem15  9771  dfac5lem1  10137  zorn2lem6  10515  cju  12236  ixxin  13379  elfzo2  13679  xpcogend  14993  summo  15733  prodmo  15952  dfiso2  17785  issubmd  18784  gsumval3eu  19885  dvdsrtr  20328  isirred2  20381  domnmuln0  20669  isdomn3  20675  abvn0b  20796  lspsolvlem  21103  unocv  21640  pf1ind  22293  ordtrest2lem  23141  lmmo  23318  ptbasin  23515  txbasval  23544  txcnp  23558  txlm  23586  tx1stc  23588  tx2ndc  23589  isfild  23796  txflf  23944  isclmp  25048  mbfi1flimlem  25675  iblcnlem1  25741  iblre  25747  iblcn  25752  logfaclbnd  27185  axcontlem4  28946  axcontlem7  28949  ocsh  31264  pjhthmo  31283  5oalem6  31640  cvnbtwn4  32270  superpos  32335  cdj3i  32422  13an22anass  32445  smatrcl  33827  ordtrest2NEWlem  33953  cusgr3cyclex  35158  lineext  36094  outsideoftr  36147  hilbert1.2  36173  lineintmo  36175  neibastop1  36377  bj-inrab  36945  isbasisrelowllem1  37373  isbasisrelowllem2  37374  ptrest  37643  poimirlem26  37670  ismblfin  37685  unirep  37738  inixp  37752  ablo4pnp  37904  keridl  38056  ispridlc  38094  anan  38247  disjecxrn  38407  coss1cnvres  38435  br1cosscnvxrn  38492  dfeldisj3  38737  antisymrelres  38781  prtlem70  38875  lcvbr3  39041  cvrnbtwn4  39297  linepsubN  39771  pmapsub  39787  pmapjoin  39871  ltrnu  40140  diblsmopel  41190  pell1234qrmulcl  42878  ifpan23  43484  ifpidg  43515  ifpbibib  43534  uneqsn  44049  isthincd2  49323