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  3200  reu2  3685  rmo4  3690  rmo3f  3694  rmo3  3841  2reu1  3849  2reu4lem  4473  disjiun  5080  inxp  5774  inxpOLD  5775  xp11  6124  dfpo2  6244  fununi  6557  fun  6686  resoprab2  7468  sorpsscmpl  7670  xporderlem  8060  poxp  8061  poseq  8091  fprlem1  8233  frrlem15  9653  dfac5lem1  10017  zorn2lem6  10395  cju  12124  ixxin  13265  elfzo2  13565  xpcogend  14881  summo  15624  prodmo  15843  dfiso2  17679  issubmd  18680  gsumval3eu  19783  dvdsrtr  20253  isirred2  20306  domnmuln0  20594  isdomn3  20600  abvn0b  20721  lspsolvlem  21049  unocv  21587  pf1ind  22240  ordtrest2lem  23088  lmmo  23265  ptbasin  23462  txbasval  23491  txcnp  23505  txlm  23533  tx1stc  23535  tx2ndc  23536  isfild  23743  txflf  23891  isclmp  24995  mbfi1flimlem  25621  iblcnlem1  25687  iblre  25693  iblcn  25698  logfaclbnd  27131  axcontlem4  28916  axcontlem7  28919  ocsh  31231  pjhthmo  31250  5oalem6  31607  cvnbtwn4  32237  superpos  32302  cdj3i  32389  13an22anass  32412  smatrcl  33779  ordtrest2NEWlem  33905  cusgr3cyclex  35129  lineext  36070  outsideoftr  36123  hilbert1.2  36149  lineintmo  36151  neibastop1  36353  bj-inrab  36921  isbasisrelowllem1  37349  isbasisrelowllem2  37350  ptrest  37619  poimirlem26  37646  ismblfin  37661  unirep  37714  inixp  37728  ablo4pnp  37880  keridl  38032  ispridlc  38070  anan  38223  disjecxrn  38381  coss1cnvres  38414  br1cosscnvxrn  38471  dfeldisj3  38717  antisymrelres  38761  prtlem70  38856  lcvbr3  39022  cvrnbtwn4  39278  linepsubN  39751  pmapsub  39767  pmapjoin  39851  ltrnu  40120  diblsmopel  41170  pell1234qrmulcl  42848  ifpan23  43453  ifpidg  43484  ifpbibib  43503  uneqsn  44018  isthincd2  49442