Theorem an4 653

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 469	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
2		an12 642	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
3	2	bianass 639	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))
4	1, 3	bitri 274	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Syntax hints:   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  an42  654  an4s  657  anandi  673  anandir  674  an6  1444  an33reanOLD  1483  reeanlem  3292  reu2  3660  rmo4  3665  rmo3f  3669  rmo3  3822  2reu1  3830  2reu4lem  4456  disjiun  5061  inxp  5741  xp11  6078  dfpo2  6199  fununi  6509  fun  6636  resoprab2  7393  sorpsscmpl  7587  xporderlem  7968  poxp  7969  fprlem1  8116  frrlem15  9515  dfac5lem1  9879  zorn2lem6  10257  cju  11969  ixxin  13096  elfzo2  13390  xpcogend  14685  summo  15429  prodmo  15646  dfiso2  17484  issubmd  18445  gsumval3eu  19505  dvdsrtr  19894  isirred2  19943  lspsolvlem  20404  domnmuln0  20569  abvn0b  20573  unocv  20885  pf1ind  21521  ordtrest2lem  22354  lmmo  22531  ptbasin  22728  txbasval  22757  txcnp  22771  txlm  22799  tx1stc  22801  tx2ndc  22802  isfild  23009  txflf  23157  isclmp  24260  mbfi1flimlem  24887  iblcnlem1  24952  iblre  24958  iblcn  24963  logfaclbnd  26370  axcontlem4  27335  axcontlem7  27338  ocsh  29645  pjhthmo  29664  5oalem6  30021  cvnbtwn4  30651  superpos  30716  cdj3i  30803  smatrcl  31746  ordtrest2NEWlem  31872  cusgr3cyclex  33098  poseq  33802  lineext  34378  outsideoftr  34431  hilbert1.2  34457  lineintmo  34459  neibastop1  34548  bj-inrab  35115  isbasisrelowllem1  35526  isbasisrelowllem2  35527  ptrest  35776  poimirlem26  35803  ismblfin  35818  unirep  35871  inixp  35886  ablo4pnp  36038  keridl  36190  ispridlc  36228  anan  36379  br1cosscnvxrn  36592  dfeldisj3  36830  prtlem70  36871  lcvbr3  37037  cvrnbtwn4  37293  linepsubN  37766  pmapsub  37782  pmapjoin  37866  ltrnu  38135  diblsmopel  39185  pell1234qrmulcl  40677  isdomn3  41029  ifpan23  41067  ifpidg  41098  ifpbibib  41117  uneqsn  41633  isthincd2  46319