Theorem an4 654

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 469	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
2		an12 643	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
3	2	bianass 640	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))
4	1, 3	bitri 274	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Syntax hints:   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  an42  655  an4s  658  anandi  674  anandir  675  an6  1445  an33reanOLD  1484  reeanlem  3224  reu2  3717  rmo4  3722  rmo3f  3726  rmo3  3879  2reu1  3887  2reu4lem  4519  disjiun  5128  inxp  5824  xp11  6163  dfpo2  6284  fununi  6612  fun  6740  resoprab2  7511  sorpsscmpl  7707  xporderlem  8095  poxp  8096  poseq  8126  fprlem1  8267  frrlem15  9734  dfac5lem1  10100  zorn2lem6  10478  cju  12190  ixxin  13323  elfzo2  13617  xpcogend  14903  summo  15645  prodmo  15862  dfiso2  17701  issubmd  18663  gsumval3eu  19731  dvdsrtr  20134  isirred2  20185  lspsolvlem  20704  domnmuln0  20850  abvn0b  20854  unocv  21166  pf1ind  21803  ordtrest2lem  22636  lmmo  22813  ptbasin  23010  txbasval  23039  txcnp  23053  txlm  23081  tx1stc  23083  tx2ndc  23084  isfild  23291  txflf  23439  isclmp  24542  mbfi1flimlem  25169  iblcnlem1  25234  iblre  25240  iblcn  25245  logfaclbnd  26652  axcontlem4  28090  axcontlem7  28093  ocsh  30399  pjhthmo  30418  5oalem6  30775  cvnbtwn4  31405  superpos  31470  cdj3i  31557  13an22anass  31569  smatrcl  32607  ordtrest2NEWlem  32733  cusgr3cyclex  33958  lineext  34878  outsideoftr  34931  hilbert1.2  34957  lineintmo  34959  neibastop1  35048  bj-inrab  35611  isbasisrelowllem1  36040  isbasisrelowllem2  36041  ptrest  36291  poimirlem26  36318  ismblfin  36333  unirep  36386  inixp  36401  ablo4pnp  36553  keridl  36705  ispridlc  36743  anan  36898  disjecxrn  37064  coss1cnvres  37092  br1cosscnvxrn  37149  dfeldisj3  37394  antisymrelres  37438  prtlem70  37532  lcvbr3  37698  cvrnbtwn4  37954  linepsubN  38428  pmapsub  38444  pmapjoin  38528  ltrnu  38797  diblsmopel  39847  pell1234qrmulcl  41364  isdomn3  41717  ifpan23  41982  ifpidg  42013  ifpbibib  42032  uneqsn  42547  isthincd2  47306