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  1444  reeanlem  3225  reu2  3733  rmo4  3738  rmo3f  3742  rmo3  3897  2reu1  3905  2reu4lem  4527  disjiun  5135  inxp  5844  inxpOLD  5845  xp11  6196  dfpo2  6317  fununi  6642  fun  6770  resoprab2  7551  sorpsscmpl  7752  xporderlem  8150  poxp  8151  poseq  8181  fprlem1  8323  frrlem15  9794  dfac5lem1  10160  zorn2lem6  10538  cju  12259  ixxin  13400  elfzo2  13698  xpcogend  15009  summo  15749  prodmo  15968  dfiso2  17819  issubmd  18831  gsumval3eu  19936  dvdsrtr  20384  isirred2  20437  domnmuln0  20725  isdomn3  20731  abvn0b  20853  lspsolvlem  21161  unocv  21715  pf1ind  22374  ordtrest2lem  23226  lmmo  23403  ptbasin  23600  txbasval  23629  txcnp  23643  txlm  23671  tx1stc  23673  tx2ndc  23674  isfild  23881  txflf  24029  isclmp  25143  mbfi1flimlem  25771  iblcnlem1  25837  iblre  25843  iblcn  25848  logfaclbnd  27280  axcontlem4  28996  axcontlem7  28999  ocsh  31311  pjhthmo  31330  5oalem6  31687  cvnbtwn4  32317  superpos  32382  cdj3i  32469  13an22anass  32492  smatrcl  33756  ordtrest2NEWlem  33882  cusgr3cyclex  35120  lineext  36057  outsideoftr  36110  hilbert1.2  36136  lineintmo  36138  neibastop1  36341  bj-inrab  36909  isbasisrelowllem1  37337  isbasisrelowllem2  37338  ptrest  37605  poimirlem26  37632  ismblfin  37647  unirep  37700  inixp  37714  ablo4pnp  37866  keridl  38018  ispridlc  38056  anan  38209  disjecxrn  38370  coss1cnvres  38398  br1cosscnvxrn  38455  dfeldisj3  38700  antisymrelres  38744  prtlem70  38838  lcvbr3  39004  cvrnbtwn4  39260  linepsubN  39734  pmapsub  39750  pmapjoin  39834  ltrnu  40103  diblsmopel  41153  pell1234qrmulcl  42842  ifpan23  43449  ifpidg  43480  ifpbibib  43499  uneqsn  44014  isthincd2  48837