Theorem an4 860

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 833	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
2	1	anbi2i 725	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃))))
3		anass 678	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
4		anass 678	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃))))
5	2, 3, 4	3bitr4i 290	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Syntax hints:   ↔ wb 194   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  an42  861  an4s  864  anandi  866  anandir  867  an6  1399  an33rean  1437  reean  3084  reu2  3360  rmo4  3365  rmo3  3493  disjiun  4567  inxp  5164  xp11  5474  fununi  5864  fun  5965  resoprab2  6633  sorpsscmpl  6823  xporderlem  7152  poxp  7153  dfac5lem1  8806  zorn2lem6  9183  cju  10863  ixxin  12019  elfzo2  12297  xpcogend  13507  summo  14241  prodmo  14451  dfiso2  16201  issubmd  17118  gsumval3eu  18074  dvdsrtr  18421  isirred2  18470  lspsolvlem  18909  domnmuln0  19065  abvn0b  19069  pf1ind  19486  unocv  19785  ordtrest2lem  20759  lmmo  20936  ptbasin  21132  txbasval  21161  txcnp  21175  txlm  21203  tx1stc  21205  tx2ndc  21206  isfild  21414  txflf  21562  isclmp  22636  mbfi1flimlem  23212  iblcnlem1  23277  iblre  23283  iblcn  23288  logfaclbnd  24664  axcontlem4  25565  axcontlem7  25568  ocsh  27332  pjhthmo  27351  5oalem6  27708  cvnbtwn4  28338  superpos  28403  cdj3i  28490  rmo3f  28525  rmo4fOLD  28526  smatrcl  28996  ordtrest2NEWlem  29102  dfpo2  30704  poseq  30800  lineext  31159  outsideoftr  31212  hilbert1.2  31238  lineintmo  31240  neibastop1  31330  bj-inrab  31911  isbasisrelowllem1  32175  isbasisrelowllem2  32176  ptrest  32374  poimirlem26  32401  ismblfin  32416  unirep  32473  inixp  32489  ablo4pnp  32645  keridl  32797  ispridlc  32835  prtlem70  32953  lcvbr3  33124  cvrnbtwn4  33380  linepsubN  33852  pmapsub  33868  pmapjoin  33952  ltrnu  34221  diblsmopel  35274  pell1234qrmulcl  36233  isdomn3  36597  ifpan23  36619  ifpidg  36651  ifpbibib  36670  uneqsn  37137  2reu1  39632  2reu4a  39635