Theorem an4 654

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 471	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
2		an12 643	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
3	2	bianass 640	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))
4	1, 3	bitri 277	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  an42  655  an4s  658  anandi  674  anandir  675  an6  1441  an33rean  1479  reeanlem  3366  reu2  3716  rmo4  3721  rmo3f  3725  rmo3  3872  rmo3OLD  3873  2reu1  3881  2reu4lem  4465  disjiun  5046  inxp  5698  xp11  6027  fununi  6424  fun  6535  resoprab2  7265  sorpsscmpl  7454  xporderlem  7815  poxp  7816  dfac5lem1  9543  zorn2lem6  9917  cju  11628  ixxin  12749  elfzo2  13035  xpcogend  14328  summo  15068  prodmo  15284  dfiso2  17036  issubmd  17965  gsumval3eu  19018  dvdsrtr  19396  isirred2  19445  lspsolvlem  19908  domnmuln0  20065  abvn0b  20069  pf1ind  20512  unocv  20818  ordtrest2lem  21805  lmmo  21982  ptbasin  22179  txbasval  22208  txcnp  22222  txlm  22250  tx1stc  22252  tx2ndc  22253  isfild  22460  txflf  22608  isclmp  23695  mbfi1flimlem  24317  iblcnlem1  24382  iblre  24388  iblcn  24393  logfaclbnd  25792  axcontlem4  26747  axcontlem7  26750  ocsh  29054  pjhthmo  29073  5oalem6  29430  cvnbtwn4  30060  superpos  30125  cdj3i  30212  smatrcl  31056  ordtrest2NEWlem  31160  cusgr3cyclex  32378  dfpo2  32986  poseq  33090  fprlem1  33132  frrlem15  33137  lineext  33532  outsideoftr  33585  hilbert1.2  33611  lineintmo  33613  neibastop1  33702  bj-inrab  34240  isbasisrelowllem1  34630  isbasisrelowllem2  34631  ptrest  34885  poimirlem26  34912  ismblfin  34927  unirep  34982  inixp  34997  ablo4pnp  35152  keridl  35304  ispridlc  35342  anan  35493  br1cosscnvxrn  35708  dfeldisj3  35946  prtlem70  35987  lcvbr3  36153  cvrnbtwn4  36409  linepsubN  36882  pmapsub  36898  pmapjoin  36982  ltrnu  37251  diblsmopel  38301  pell1234qrmulcl  39445  isdomn3  39797  ifpan23  39818  ifpidg  39850  ifpbibib  39869  uneqsn  40366