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 469	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
2		an12 643	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
3	2	bianass 640	. 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  655  an4s  658  anandi  674  anandir  675  an6  1445  an33reanOLD  1484  reeanlem  3225  reu2  3720  rmo4  3725  rmo3f  3729  rmo3  3882  2reu1  3890  2reu4lem  4524  disjiun  5134  inxp  5830  xp11  6171  dfpo2  6292  fununi  6620  fun  6750  resoprab2  7523  sorpsscmpl  7720  xporderlem  8109  poxp  8110  poseq  8140  fprlem1  8281  frrlem15  9748  dfac5lem1  10114  zorn2lem6  10492  cju  12204  ixxin  13337  elfzo2  13631  xpcogend  14917  summo  15659  prodmo  15876  dfiso2  17715  issubmd  18683  gsumval3eu  19766  dvdsrtr  20174  isirred2  20227  lspsolvlem  20747  domnmuln0  20906  abvn0b  20912  unocv  21224  pf1ind  21865  ordtrest2lem  22698  lmmo  22875  ptbasin  23072  txbasval  23101  txcnp  23115  txlm  23143  tx1stc  23145  tx2ndc  23146  isfild  23353  txflf  23501  isclmp  24604  mbfi1flimlem  25231  iblcnlem1  25296  iblre  25302  iblcn  25307  logfaclbnd  26714  axcontlem4  28214  axcontlem7  28217  ocsh  30523  pjhthmo  30542  5oalem6  30899  cvnbtwn4  31529  superpos  31594  cdj3i  31681  13an22anass  31693  smatrcl  32764  ordtrest2NEWlem  32890  cusgr3cyclex  34115  lineext  35036  outsideoftr  35089  hilbert1.2  35115  lineintmo  35117  neibastop1  35232  bj-inrab  35795  isbasisrelowllem1  36224  isbasisrelowllem2  36225  ptrest  36475  poimirlem26  36502  ismblfin  36517  unirep  36570  inixp  36584  ablo4pnp  36736  keridl  36888  ispridlc  36926  anan  37081  disjecxrn  37247  coss1cnvres  37275  br1cosscnvxrn  37332  dfeldisj3  37577  antisymrelres  37621  prtlem70  37715  lcvbr3  37881  cvrnbtwn4  38137  linepsubN  38611  pmapsub  38627  pmapjoin  38711  ltrnu  38980  diblsmopel  40030  pell1234qrmulcl  41578  isdomn3  41931  ifpan23  42196  ifpidg  42227  ifpbibib  42246  uneqsn  42761  isthincd2  47611