Theorem an4 657

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 646	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
3	2	bianass 643	. 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  658  an4s  661  anandi  677  anandir  678  an6  1448  reeanlem  3209  reu2  3672  rmo4  3677  rmo3f  3681  rmo3  3828  2reu1  3836  2reu4lem  4464  disjiun  5074  inxp  5780  inxpOLD  5781  xp11  6133  dfpo2  6254  fununi  6567  fun  6696  resoprab2  7479  sorpsscmpl  7681  xporderlem  8070  poxp  8071  poseq  8101  fprlem1  8243  frrlem15  9672  dfac5lem1  10036  zorn2lem6  10414  cju  12146  ixxin  13306  elfzo2  13607  xpcogend  14927  summo  15670  prodmo  15892  dfiso2  17730  issubmd  18765  gsumval3eu  19870  dvdsrtr  20339  isirred2  20392  domnmuln0  20677  isdomn3  20683  abvn0b  20804  lspsolvlem  21132  unocv  21670  pf1ind  22330  ordtrest2lem  23178  lmmo  23355  ptbasin  23552  txbasval  23581  txcnp  23595  txlm  23623  tx1stc  23625  tx2ndc  23626  isfild  23833  txflf  23981  isclmp  25074  mbfi1flimlem  25699  iblcnlem1  25765  iblre  25771  iblcn  25776  logfaclbnd  27199  ons2ind  28281  axcontlem4  29050  axcontlem7  29053  ocsh  31369  pjhthmo  31388  5oalem6  31745  cvnbtwn4  32375  superpos  32440  cdj3i  32527  13an22anass  32548  smatrcl  33956  ordtrest2NEWlem  34082  cusgr3cyclex  35334  lineext  36274  outsideoftr  36327  hilbert1.2  36353  lineintmo  36355  neibastop1  36557  bj-inrab  37250  isbasisrelowllem1  37685  isbasisrelowllem2  37686  ptrest  37954  poimirlem26  37981  ismblfin  37996  unirep  38049  inixp  38063  ablo4pnp  38215  keridl  38367  ispridlc  38405  anan  38570  disjecxrn  38747  coss1cnvres  38842  br1cosscnvxrn  38899  dfeldisj3  39146  antisymrelres  39201  prtlem70  39317  lcvbr3  39483  cvrnbtwn4  39739  linepsubN  40212  pmapsub  40228  pmapjoin  40312  ltrnu  40581  diblsmopel  41631  pell1234qrmulcl  43301  ifpan23  43905  ifpidg  43936  ifpbibib  43955  uneqsn  44470  isthincd2  49924