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  3203  reu2  3679  rmo4  3684  rmo3f  3688  rmo3  3835  2reu1  3843  2reu4lem  4467  disjiun  5074  inxp  5766  inxpOLD  5767  xp11  6117  dfpo2  6238  fununi  6551  fun  6680  resoprab2  7460  sorpsscmpl  7662  xporderlem  8052  poxp  8053  poseq  8083  fprlem1  8225  frrlem15  9645  dfac5lem1  10009  zorn2lem6  10387  cju  12116  ixxin  13257  elfzo2  13557  xpcogend  14876  summo  15619  prodmo  15838  dfiso2  17674  issubmd  18709  gsumval3eu  19811  dvdsrtr  20281  isirred2  20334  domnmuln0  20619  isdomn3  20625  abvn0b  20746  lspsolvlem  21074  unocv  21612  pf1ind  22265  ordtrest2lem  23113  lmmo  23290  ptbasin  23487  txbasval  23516  txcnp  23530  txlm  23558  tx1stc  23560  tx2ndc  23561  isfild  23768  txflf  23916  isclmp  25019  mbfi1flimlem  25645  iblcnlem1  25711  iblre  25717  iblcn  25722  logfaclbnd  27155  axcontlem4  28940  axcontlem7  28943  ocsh  31255  pjhthmo  31274  5oalem6  31631  cvnbtwn4  32261  superpos  32326  cdj3i  32413  13an22anass  32435  smatrcl  33801  ordtrest2NEWlem  33927  cusgr3cyclex  35172  lineext  36110  outsideoftr  36163  hilbert1.2  36189  lineintmo  36191  neibastop1  36393  bj-inrab  36961  isbasisrelowllem1  37389  isbasisrelowllem2  37390  ptrest  37659  poimirlem26  37686  ismblfin  37701  unirep  37754  inixp  37768  ablo4pnp  37920  keridl  38072  ispridlc  38110  anan  38263  disjecxrn  38421  coss1cnvres  38454  br1cosscnvxrn  38511  dfeldisj3  38757  antisymrelres  38801  prtlem70  38896  lcvbr3  39062  cvrnbtwn4  39318  linepsubN  39791  pmapsub  39807  pmapjoin  39891  ltrnu  40160  diblsmopel  41210  pell1234qrmulcl  42888  ifpan23  43493  ifpidg  43524  ifpbibib  43543  uneqsn  44058  isthincd2  49469