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  3207  reu2  3683  rmo4  3688  rmo3f  3692  rmo3  3839  2reu1  3847  2reu4lem  4476  disjiun  5086  inxp  5780  inxpOLD  5781  xp11  6133  dfpo2  6254  fununi  6567  fun  6696  resoprab2  7477  sorpsscmpl  7679  xporderlem  8069  poxp  8070  poseq  8100  fprlem1  8242  frrlem15  9669  dfac5lem1  10033  zorn2lem6  10411  cju  12141  ixxin  13278  elfzo2  13578  xpcogend  14897  summo  15640  prodmo  15859  dfiso2  17696  issubmd  18731  gsumval3eu  19833  dvdsrtr  20304  isirred2  20357  domnmuln0  20642  isdomn3  20648  abvn0b  20769  lspsolvlem  21097  unocv  21635  pf1ind  22299  ordtrest2lem  23147  lmmo  23324  ptbasin  23521  txbasval  23550  txcnp  23564  txlm  23592  tx1stc  23594  tx2ndc  23595  isfild  23802  txflf  23950  isclmp  25053  mbfi1flimlem  25679  iblcnlem1  25745  iblre  25751  iblcn  25756  logfaclbnd  27189  ons2ind  28271  axcontlem4  29040  axcontlem7  29043  ocsh  31358  pjhthmo  31377  5oalem6  31734  cvnbtwn4  32364  superpos  32429  cdj3i  32516  13an22anass  32538  smatrcl  33953  ordtrest2NEWlem  34079  cusgr3cyclex  35330  lineext  36270  outsideoftr  36323  hilbert1.2  36349  lineintmo  36351  neibastop1  36553  bj-inrab  37128  isbasisrelowllem1  37560  isbasisrelowllem2  37561  ptrest  37820  poimirlem26  37847  ismblfin  37862  unirep  37915  inixp  37929  ablo4pnp  38081  keridl  38233  ispridlc  38271  anan  38431  disjecxrn  38597  coss1cnvres  38680  br1cosscnvxrn  38737  dfeldisj3  38978  antisymrelres  39022  prtlem70  39117  lcvbr3  39283  cvrnbtwn4  39539  linepsubN  40012  pmapsub  40028  pmapjoin  40112  ltrnu  40381  diblsmopel  41431  pell1234qrmulcl  43097  ifpan23  43701  ifpidg  43732  ifpbibib  43751  uneqsn  44266  isthincd2  49682