Theorem an4 655

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 644	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
3	2	bianass 641	. 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  656  an4s  659  anandi  675  anandir  676  an6  1445  reeanlem  3234  reu2  3747  rmo4  3752  rmo3f  3756  rmo3  3911  2reu1  3919  2reu4lem  4545  disjiun  5154  inxp  5856  inxpOLD  5857  xp11  6206  dfpo2  6327  fununi  6653  fun  6783  resoprab2  7569  sorpsscmpl  7769  xporderlem  8168  poxp  8169  poseq  8199  fprlem1  8341  frrlem15  9826  dfac5lem1  10192  zorn2lem6  10570  cju  12289  ixxin  13424  elfzo2  13719  xpcogend  15023  summo  15765  prodmo  15984  dfiso2  17833  issubmd  18841  gsumval3eu  19946  dvdsrtr  20394  isirred2  20447  domnmuln0  20731  isdomn3  20737  abvn0b  20859  lspsolvlem  21167  unocv  21721  pf1ind  22380  ordtrest2lem  23232  lmmo  23409  ptbasin  23606  txbasval  23635  txcnp  23649  txlm  23677  tx1stc  23679  tx2ndc  23680  isfild  23887  txflf  24035  isclmp  25149  mbfi1flimlem  25777  iblcnlem1  25843  iblre  25849  iblcn  25854  logfaclbnd  27284  axcontlem4  29000  axcontlem7  29003  ocsh  31315  pjhthmo  31334  5oalem6  31691  cvnbtwn4  32321  superpos  32386  cdj3i  32473  13an22anass  32493  smatrcl  33742  ordtrest2NEWlem  33868  cusgr3cyclex  35104  lineext  36040  outsideoftr  36093  hilbert1.2  36119  lineintmo  36121  neibastop1  36325  bj-inrab  36893  isbasisrelowllem1  37321  isbasisrelowllem2  37322  ptrest  37579  poimirlem26  37606  ismblfin  37621  unirep  37674  inixp  37688  ablo4pnp  37840  keridl  37992  ispridlc  38030  anan  38183  disjecxrn  38345  coss1cnvres  38373  br1cosscnvxrn  38430  dfeldisj3  38675  antisymrelres  38719  prtlem70  38813  lcvbr3  38979  cvrnbtwn4  39235  linepsubN  39709  pmapsub  39725  pmapjoin  39809  ltrnu  40078  diblsmopel  41128  pell1234qrmulcl  42811  ifpan23  43422  ifpidg  43453  ifpbibib  43472  uneqsn  43987  isthincd2  48705