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  3233  reu2  3683  rmo4  3688  rmo3f  3692  rmo3  3836  2reu1  3845  2reu4lem  4479  disjiun  5091  inxp  5812  xp11  6168  dfpo2  6294  fununi  6608  fun  6737  resoprab2  7532  sorpsscmpl  7735  xporderlem  8125  poxp  8126  poseq  8156  fprlem1  8299  frrlem15  9739  dfac5lem1  10126  zorn2lem6  10503  cju  12238  ixxin  13415  elfzo2  13717  xpcogend  15047  summo  15803  prodmo  16023  dfiso2  17861  issubmd  18914  gsumval3eu  20031  dvdsrtr  20509  isirred2  20562  domnmuln0  20871  isdomn3  20876  abvn0b  21002  lspsolvlem  21329  unocv  21893  pf1ind  22580  ordtrest2lem  23428  lmmo  23605  ptbasin  23803  txbasval  23832  txcnp  23846  txlm  23874  tx1stc  23876  tx2ndc  23877  isfild  24084  txflf  24232  isclmp  25325  mbfi1flimlem  25950  iblcnlem1  26015  iblre  26021  iblcn  26026  logfaclbnd  27458  ons2ind  28540  axcontlem4  29424  axcontlem7  29427  ocsh  31764  pjhthmo  31783  5oalem6  32140  cvnbtwn4  32770  superpos  32835  cdj3i  32922  smatrcl  34306  ordtrest2NEWlem  34432  cusgr3cyclex  35725  lineext  36656  outsideoftr  36709  hilbert1.2  36735  lineintmo  36737  neibastop1  36978  bj-inrab  37671  isbasisrelowllem1  38109  isbasisrelowllem2  38110  ptrest  38368  poimirlem26  38395  ismblfin  38410  unirep  38464  inixp  38478  ablo4pnp  38630  keridl  38782  ispridlc  38820  anan  38983  disjecxrn  39160  coss1cnvres  39255  br1cosscnvxrn  39312  dfeldisj3  39559  antisymrelres  39614  prtlem70  39730  lcvbr3  39896  cvrnbtwn4  40152  linepsubN  40625  pmapsub  40641  pmapjoin  40725  ltrnu  40994  diblsmopel  42044  pell1234qrmulcl  43696  ifpan23  44300  ifpidg  44331  ifpbibib  44350  uneqsn  44865  isthincd2  50363