Theorem an4 652

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

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  an42  653  an4s  656  anandi  672  anandir  673  an6  1443  an33reanOLD  1482  reeanlem  3290  reu2  3655  rmo4  3660  rmo3f  3664  rmo3  3818  2reu1  3826  2reu4lem  4453  disjiun  5057  inxp  5730  xp11  6067  dfpo2  6188  fununi  6493  fun  6620  resoprab2  7371  sorpsscmpl  7565  xporderlem  7939  poxp  7940  fprlem1  8087  frrlem15  9446  dfac5lem1  9810  zorn2lem6  10188  cju  11899  ixxin  13025  elfzo2  13319  xpcogend  14613  summo  15357  prodmo  15574  dfiso2  17401  issubmd  18360  gsumval3eu  19420  dvdsrtr  19809  isirred2  19858  lspsolvlem  20319  domnmuln0  20482  abvn0b  20486  unocv  20797  pf1ind  21431  ordtrest2lem  22262  lmmo  22439  ptbasin  22636  txbasval  22665  txcnp  22679  txlm  22707  tx1stc  22709  tx2ndc  22710  isfild  22917  txflf  23065  isclmp  24166  mbfi1flimlem  24792  iblcnlem1  24857  iblre  24863  iblcn  24868  logfaclbnd  26275  axcontlem4  27238  axcontlem7  27241  ocsh  29546  pjhthmo  29565  5oalem6  29922  cvnbtwn4  30552  superpos  30617  cdj3i  30704  smatrcl  31648  ordtrest2NEWlem  31774  cusgr3cyclex  32998  poseq  33729  lineext  34305  outsideoftr  34358  hilbert1.2  34384  lineintmo  34386  neibastop1  34475  bj-inrab  35042  isbasisrelowllem1  35453  isbasisrelowllem2  35454  ptrest  35703  poimirlem26  35730  ismblfin  35745  unirep  35798  inixp  35813  ablo4pnp  35965  keridl  36117  ispridlc  36155  anan  36306  br1cosscnvxrn  36519  dfeldisj3  36757  prtlem70  36798  lcvbr3  36964  cvrnbtwn4  37220  linepsubN  37693  pmapsub  37709  pmapjoin  37793  ltrnu  38062  diblsmopel  39112  pell1234qrmulcl  40593  isdomn3  40945  ifpan23  40965  ifpidg  40996  ifpbibib  41015  uneqsn  41522  isthincd2  46207