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 472	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
2		an12 644	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
3	2	bianass 641	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))
4	1, 3	bitri 278	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Syntax hints:   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  an42  656  an4s  659  anandi  675  anandir  676  an6  1442  an33reanOLD  1481  reeanlem  3283  reu2  3639  rmo4  3644  rmo3f  3648  rmo3  3795  2reu1  3803  2reu4lem  4418  disjiun  5019  inxp  5672  xp11  6004  fununi  6410  fun  6525  resoprab2  7265  sorpsscmpl  7458  xporderlem  7826  poxp  7827  dfac5lem1  9583  zorn2lem6  9961  cju  11670  ixxin  12796  elfzo2  13090  xpcogend  14381  summo  15122  prodmo  15338  dfiso2  17101  issubmd  18037  gsumval3eu  19092  dvdsrtr  19473  isirred2  19522  lspsolvlem  19982  domnmuln0  20139  abvn0b  20143  unocv  20445  pf1ind  21074  ordtrest2lem  21903  lmmo  22080  ptbasin  22277  txbasval  22306  txcnp  22320  txlm  22348  tx1stc  22350  tx2ndc  22351  isfild  22558  txflf  22706  isclmp  23798  mbfi1flimlem  24422  iblcnlem1  24487  iblre  24493  iblcn  24498  logfaclbnd  25905  axcontlem4  26860  axcontlem7  26863  ocsh  29165  pjhthmo  29184  5oalem6  29541  cvnbtwn4  30171  superpos  30236  cdj3i  30323  smatrcl  31267  ordtrest2NEWlem  31393  cusgr3cyclex  32614  dfpo2  33238  poseq  33356  fprlem1  33398  frrlem15  33403  lineext  33927  outsideoftr  33980  hilbert1.2  34006  lineintmo  34008  neibastop1  34097  bj-inrab  34650  isbasisrelowllem1  35052  isbasisrelowllem2  35053  ptrest  35336  poimirlem26  35363  ismblfin  35378  unirep  35431  inixp  35446  ablo4pnp  35598  keridl  35750  ispridlc  35788  anan  35939  br1cosscnvxrn  36154  dfeldisj3  36392  prtlem70  36433  lcvbr3  36599  cvrnbtwn4  36855  linepsubN  37328  pmapsub  37344  pmapjoin  37428  ltrnu  37697  diblsmopel  38747  pell1234qrmulcl  40169  isdomn3  40521  ifpan23  40541  ifpidg  40572  ifpbibib  40591  uneqsn  41099