Theorem an4 882

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 855	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
2	1	anbi2i 730	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃))))
3		anass 682	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
4		anass 682	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃))))
5	2, 3, 4	3bitr4i 292	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Syntax hints:   ↔ wb 196   ∧ 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 197  df-an 385

This theorem is referenced by:  an42  883  an4s  886  anandi  888  anandir  889  an6  1448  an33rean  1486  reean  3135  reu2  3427  rmo4  3432  rmo3  3561  disjiun  4672  inxp  5287  xp11  5604  fununi  6002  fun  6104  resoprab2  6799  sorpsscmpl  6990  xporderlem  7333  poxp  7334  dfac5lem1  8984  zorn2lem6  9361  cju  11054  ixxin  12230  elfzo2  12512  xpcogend  13759  summo  14492  prodmo  14710  dfiso2  16479  issubmd  17396  gsumval3eu  18351  dvdsrtr  18698  isirred2  18747  lspsolvlem  19190  domnmuln0  19346  abvn0b  19350  pf1ind  19767  unocv  20072  ordtrest2lem  21055  lmmo  21232  ptbasin  21428  txbasval  21457  txcnp  21471  txlm  21499  tx1stc  21501  tx2ndc  21502  isfild  21709  txflf  21857  isclmp  22943  mbfi1flimlem  23534  iblcnlem1  23599  iblre  23605  iblcn  23610  logfaclbnd  24992  axcontlem4  25892  axcontlem7  25895  ocsh  28270  pjhthmo  28289  5oalem6  28646  cvnbtwn4  29276  superpos  29341  cdj3i  29428  rmo3f  29462  rmo4fOLD  29463  smatrcl  29990  ordtrest2NEWlem  30096  dfpo2  31771  poseq  31878  lineext  32308  outsideoftr  32361  hilbert1.2  32387  lineintmo  32389  neibastop1  32479  bj-inrab  33048  isbasisrelowllem1  33333  isbasisrelowllem2  33334  ptrest  33538  poimirlem26  33565  ismblfin  33580  unirep  33637  inixp  33653  ablo4pnp  33809  keridl  33961  ispridlc  33999  anan  34142  br1cosscnvxrn  34364  prtlem70  34460  lcvbr3  34628  cvrnbtwn4  34884  linepsubN  35356  pmapsub  35372  pmapjoin  35456  ltrnu  35725  diblsmopel  36777  pell1234qrmulcl  37736  isdomn3  38099  ifpan23  38121  ifpidg  38153  ifpbibib  38172  uneqsn  38638  2reu1  41507  2reu4a  41510