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  3685  rmo4  3690  rmo3f  3694  rmo3  3841  2reu1  3849  2reu4lem  4478  disjiun  5088  inxp  5788  inxpOLD  5789  xp11  6141  dfpo2  6262  fununi  6575  fun  6704  resoprab2  7487  sorpsscmpl  7689  xporderlem  8079  poxp  8080  poseq  8110  fprlem1  8252  frrlem15  9681  dfac5lem1  10045  zorn2lem6  10423  cju  12153  ixxin  13290  elfzo2  13590  xpcogend  14909  summo  15652  prodmo  15871  dfiso2  17708  issubmd  18743  gsumval3eu  19845  dvdsrtr  20316  isirred2  20369  domnmuln0  20654  isdomn3  20660  abvn0b  20781  lspsolvlem  21109  unocv  21647  pf1ind  22311  ordtrest2lem  23159  lmmo  23336  ptbasin  23533  txbasval  23562  txcnp  23576  txlm  23604  tx1stc  23606  tx2ndc  23607  isfild  23814  txflf  23962  isclmp  25065  mbfi1flimlem  25691  iblcnlem1  25757  iblre  25763  iblcn  25768  logfaclbnd  27201  ons2ind  28283  axcontlem4  29052  axcontlem7  29055  ocsh  31370  pjhthmo  31389  5oalem6  31746  cvnbtwn4  32376  superpos  32441  cdj3i  32528  13an22anass  32549  smatrcl  33973  ordtrest2NEWlem  34099  cusgr3cyclex  35349  lineext  36289  outsideoftr  36342  hilbert1.2  36368  lineintmo  36370  neibastop1  36572  bj-inrab  37172  isbasisrelowllem1  37607  isbasisrelowllem2  37608  ptrest  37867  poimirlem26  37894  ismblfin  37909  unirep  37962  inixp  37976  ablo4pnp  38128  keridl  38280  ispridlc  38318  anan  38483  disjecxrn  38660  coss1cnvres  38755  br1cosscnvxrn  38812  dfeldisj3  39059  antisymrelres  39114  prtlem70  39230  lcvbr3  39396  cvrnbtwn4  39652  linepsubN  40125  pmapsub  40141  pmapjoin  40225  ltrnu  40494  diblsmopel  41544  pell1234qrmulcl  43209  ifpan23  43813  ifpidg  43844  ifpbibib  43863  uneqsn  44378  isthincd2  49793