Theorem an4 669

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 474	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
2		an12 658	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
3	2	bianass 655	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))
4	1, 3	bitri 278	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an42  670  an4s  673  anandi  689  anandir  690  13an22anass  1379  an6  1474  reeanlem  3238  reu2  3690  rmo4  3695  rmo3f  3699  rmo3  3843  2reu1  3852  2reu4lem  4486  disjiun  5099  inxp  5820  xp11  6175  dfpo2  6301  fununi  6615  fun  6744  resoprab2  7535  sorpsscmpl  7737  xporderlem  8125  poxp  8126  poseq  8156  fprlem1  8299  frrlem15  9732  dfac5lem1  10119  zorn2lem6  10496  cju  12225  ixxin  13400  elfzo2  13702  xpcogend  15030  summo  15786  prodmo  16008  dfiso2  17846  issubmd  18887  gsumval3eu  19997  dvdsrtr  20475  isirred2  20528  domnmuln0  20837  isdomn3  20842  abvn0b  20968  lspsolvlem  21295  unocv  21859  pf1ind  22544  ordtrest2lem  23389  lmmo  23566  ptbasin  23763  txbasval  23792  txcnp  23806  txlm  23834  tx1stc  23836  tx2ndc  23837  isfild  24044  txflf  24192  isclmp  25285  mbfi1flimlem  25910  iblcnlem1  25976  iblre  25982  iblcn  25987  logfaclbnd  27415  ons2ind  28497  axcontlem4  29346  axcontlem7  29349  ocsh  31664  pjhthmo  31683  5oalem6  32040  cvnbtwn4  32670  superpos  32735  cdj3i  32822  smatrcl  34209  ordtrest2NEWlem  34335  cusgr3cyclex  35641  lineext  36581  outsideoftr  36634  hilbert1.2  36660  lineintmo  36662  neibastop1  36903  bj-inrab  37596  isbasisrelowllem1  38034  isbasisrelowllem2  38035  ptrest  38303  poimirlem26  38330  ismblfin  38345  unirep  38398  inixp  38412  ablo4pnp  38564  keridl  38716  ispridlc  38754  anan  38917  disjecxrn  39094  coss1cnvres  39189  br1cosscnvxrn  39246  dfeldisj3  39493  antisymrelres  39548  prtlem70  39664  lcvbr3  39830  cvrnbtwn4  40086  linepsubN  40559  pmapsub  40575  pmapjoin  40659  ltrnu  40928  diblsmopel  41978  pell1234qrmulcl  43615  ifpan23  44219  ifpidg  44250  ifpbibib  44269  uneqsn  44784  isthincd2  50248