Theorem an4 669

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an42  670  an4s  673  anandi  689  anandir  690  13an22anass  1379  an6  1474  reeanlem  3233  reu2  3682  rmo4  3687  rmo3f  3691  rmo3  3835  2reu1  3844  2reu4lem  4478  disjiun  5090  inxp  5808  xp11  6166  dfpo2  6299  fununi  6616  fun  6745  resoprab2  7540  sorpsscmpl  7751  xporderlem  8142  poxp  8143  poseq  8178  fprlem1  8322  frrlem15  9765  dfac5lem1  10206  zorn2lem6  10583  cju  12320  ixxin  13497  elfzo2  13800  xpcogend  15133  summo  15889  prodmo  16109  dfiso2  17953  issubmd  19007  gsumval3eu  20124  dvdsrtr  20604  isirred2  20657  domnmuln0  20967  isdomn3  20972  abvn0b  21099  lspsolvlem  21426  unocv  21992  pf1ind  22679  ordtrest2lem  23527  lmmo  23704  ptbasin  23902  txbasval  23931  txcnp  23945  txlm  23973  tx1stc  23975  tx2ndc  23976  isfild  24183  txflf  24331  isclmp  25424  mbfi1flimlem  26049  iblcnlem1  26114  iblre  26120  iblcn  26125  logfaclbnd  27555  ons2ind  28667  axcontlem4  29551  axcontlem7  29554  ocsh  31891  pjhthmo  31910  5oalem6  32267  cvnbtwn4  32897  superpos  32962  cdj3i  33049  smatrcl  34475  ordtrest2NEWlem  34601  fwfffunres  35765  cusgr3cyclex  35988  lineext  36934  outsideoftr  36987  hilbert1.2  37013  lineintmo  37015  neibastop1  37240  bj-inrab  37933  isbasisrelowllem1  38372  isbasisrelowllem2  38373  ptrest  38631  poimirlem26  38658  ismblfin  38673  unirep  38742  inixp  38756  ablo4pnp  38908  keridl  39060  ispridlc  39098  anan  39261  disjecxrn  39438  coss1cnvres  39533  br1cosscnvxrn  39590  dfeldisj3  39837  antisymrelres  39892  prtlem70  40008  lcvbr3  40174  cvrnbtwn4  40430  linepsubN  40903  pmapsub  40919  pmapjoin  41003  ltrnu  41272  diblsmopel  42322  pell1234qrmulcl  43956  ifpan23  44555  ifpidg  44586  ifpbibib  44605  uneqsn  45119  isthincd2  50666