Theorem an4 656

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  an42  657  an4s  660  anandi  676  anandir  677  an6  1447  reeanlem  3208  reu2  3696  rmo4  3701  rmo3f  3705  rmo3  3852  2reu1  3860  2reu4lem  4485  disjiun  5095  inxp  5795  inxpOLD  5796  xp11  6148  dfpo2  6269  fununi  6591  fun  6722  resoprab2  7508  sorpsscmpl  7710  xporderlem  8106  poxp  8107  poseq  8137  fprlem1  8279  frrlem15  9710  dfac5lem1  10076  zorn2lem6  10454  cju  12182  ixxin  13323  elfzo2  13623  xpcogend  14940  summo  15683  prodmo  15902  dfiso2  17734  issubmd  18733  gsumval3eu  19834  dvdsrtr  20277  isirred2  20330  domnmuln0  20618  isdomn3  20624  abvn0b  20745  lspsolvlem  21052  unocv  21589  pf1ind  22242  ordtrest2lem  23090  lmmo  23267  ptbasin  23464  txbasval  23493  txcnp  23507  txlm  23535  tx1stc  23537  tx2ndc  23538  isfild  23745  txflf  23893  isclmp  24997  mbfi1flimlem  25623  iblcnlem1  25689  iblre  25695  iblcn  25700  logfaclbnd  27133  axcontlem4  28894  axcontlem7  28897  ocsh  31212  pjhthmo  31231  5oalem6  31588  cvnbtwn4  32218  superpos  32283  cdj3i  32370  13an22anass  32393  smatrcl  33786  ordtrest2NEWlem  33912  cusgr3cyclex  35123  lineext  36064  outsideoftr  36117  hilbert1.2  36143  lineintmo  36145  neibastop1  36347  bj-inrab  36915  isbasisrelowllem1  37343  isbasisrelowllem2  37344  ptrest  37613  poimirlem26  37640  ismblfin  37655  unirep  37708  inixp  37722  ablo4pnp  37874  keridl  38026  ispridlc  38064  anan  38217  disjecxrn  38375  coss1cnvres  38408  br1cosscnvxrn  38465  dfeldisj3  38711  antisymrelres  38755  prtlem70  38850  lcvbr3  39016  cvrnbtwn4  39272  linepsubN  39746  pmapsub  39762  pmapjoin  39846  ltrnu  40115  diblsmopel  41165  pell1234qrmulcl  42843  ifpan23  43449  ifpidg  43480  ifpbibib  43499  uneqsn  44014  isthincd2  49426