Theorem an4 861

Description: Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)

Assertion

Ref	Expression
an4	⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Proof of Theorem an4

Step	Hyp	Ref	Expression
1		an12 834	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
2	1	anbi2i 726	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃))))
3		anass 679	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
4		anass 679	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃))))
5	2, 3, 4	3bitr4i 291	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Syntax hints:   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  an42  862  an4s  865  anandi  867  anandir  868  an6  1400  an33rean  1438  reean  3085  reu2  3361  rmo4  3366  rmo3  3494  disjiun  4573  inxp  5176  xp11  5488  fununi  5878  fun  5979  resoprab2  6655  sorpsscmpl  6846  xporderlem  7175  poxp  7176  dfac5lem1  8829  zorn2lem6  9206  cju  10893  ixxin  12063  elfzo2  12342  xpcogend  13561  summo  14295  prodmo  14505  dfiso2  16255  issubmd  17172  gsumval3eu  18128  dvdsrtr  18475  isirred2  18524  lspsolvlem  18963  domnmuln0  19119  abvn0b  19123  pf1ind  19540  unocv  19843  ordtrest2lem  20817  lmmo  20994  ptbasin  21190  txbasval  21219  txcnp  21233  txlm  21261  tx1stc  21263  tx2ndc  21264  isfild  21472  txflf  21620  isclmp  22705  mbfi1flimlem  23295  iblcnlem1  23360  iblre  23366  iblcn  23371  logfaclbnd  24747  axcontlem4  25647  axcontlem7  25650  ocsh  27526  pjhthmo  27545  5oalem6  27902  cvnbtwn4  28532  superpos  28597  cdj3i  28684  rmo3f  28719  rmo4fOLD  28720  smatrcl  29190  ordtrest2NEWlem  29296  dfpo2  30898  poseq  30994  lineext  31353  outsideoftr  31406  hilbert1.2  31432  lineintmo  31434  neibastop1  31524  bj-inrab  32115  isbasisrelowllem1  32379  isbasisrelowllem2  32380  ptrest  32578  poimirlem26  32605  ismblfin  32620  unirep  32677  inixp  32693  ablo4pnp  32849  keridl  33001  ispridlc  33039  prtlem70  33157  lcvbr3  33328  cvrnbtwn4  33584  linepsubN  34056  pmapsub  34072  pmapjoin  34156  ltrnu  34425  diblsmopel  35478  pell1234qrmulcl  36437  isdomn3  36801  ifpan23  36823  ifpidg  36855  ifpbibib  36874  uneqsn  37341  2reu1  39835  2reu4a  39838