Theorem an4 657

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 646	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
3	2	bianass 643	. 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  658  an4s  661  anandi  677  anandir  678  an6  1448  reeanlem  3208  reu2  3671  rmo4  3676  rmo3f  3680  rmo3  3827  2reu1  3835  2reu4lem  4463  disjiun  5073  inxp  5787  xp11  6139  dfpo2  6260  fununi  6573  fun  6702  resoprab2  7486  sorpsscmpl  7688  xporderlem  8077  poxp  8078  poseq  8108  fprlem1  8250  frrlem15  9681  dfac5lem1  10045  zorn2lem6  10423  cju  12155  ixxin  13315  elfzo2  13616  xpcogend  14936  summo  15679  prodmo  15901  dfiso2  17739  issubmd  18774  gsumval3eu  19879  dvdsrtr  20348  isirred2  20401  domnmuln0  20686  isdomn3  20692  abvn0b  20813  lspsolvlem  21140  unocv  21660  pf1ind  22320  ordtrest2lem  23168  lmmo  23345  ptbasin  23542  txbasval  23571  txcnp  23585  txlm  23613  tx1stc  23615  tx2ndc  23616  isfild  23823  txflf  23971  isclmp  25064  mbfi1flimlem  25689  iblcnlem1  25755  iblre  25761  iblcn  25766  logfaclbnd  27185  ons2ind  28267  axcontlem4  29036  axcontlem7  29039  ocsh  31354  pjhthmo  31373  5oalem6  31730  cvnbtwn4  32360  superpos  32425  cdj3i  32512  13an22anass  32533  smatrcl  33940  ordtrest2NEWlem  34066  cusgr3cyclex  35318  lineext  36258  outsideoftr  36311  hilbert1.2  36337  lineintmo  36339  neibastop1  36541  bj-inrab  37234  isbasisrelowllem1  37671  isbasisrelowllem2  37672  ptrest  37940  poimirlem26  37967  ismblfin  37982  unirep  38035  inixp  38049  ablo4pnp  38201  keridl  38353  ispridlc  38391  anan  38556  disjecxrn  38733  coss1cnvres  38828  br1cosscnvxrn  38885  dfeldisj3  39132  antisymrelres  39187  prtlem70  39303  lcvbr3  39469  cvrnbtwn4  39725  linepsubN  40198  pmapsub  40214  pmapjoin  40298  ltrnu  40567  diblsmopel  41617  pell1234qrmulcl  43283  ifpan23  43887  ifpidg  43918  ifpbibib  43937  uneqsn  44452  isthincd2  49912