Theorem an4 666

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

Syntax hints:   ↔ wb 208   ∧ 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 209  df-an 400

This theorem is referenced by:  an42  667  an4s  670  anandi  686  anandir  687  an6  1465  reeanlem  3232  reu2  3686  rmo4  3691  rmo3f  3695  rmo3  3840  2reu1  3848  2reu4lem  4474  disjiun  5085  inxp  5800  xp11  6156  dfpo2  6278  fununi  6591  fun  6721  resoprab2  7510  sorpsscmpl  7712  xporderlem  8101  poxp  8102  poseq  8132  fprlem1  8275  frrlem15  9709  dfac5lem1  10073  zorn2lem6  10452  cju  12185  ixxin  13360  elfzo2  13661  xpcogend  14981  summo  15735  prodmo  15957  dfiso2  17796  issubmd  18831  gsumval3eu  19935  dvdsrtr  20404  isirred2  20457  domnmuln0  20746  isdomn3  20752  abvn0b  20873  lspsolvlem  21200  unocv  21720  pf1ind  22406  ordtrest2lem  23251  lmmo  23428  ptbasin  23625  txbasval  23654  txcnp  23668  txlm  23696  tx1stc  23698  tx2ndc  23699  isfild  23906  txflf  24054  isclmp  25147  mbfi1flimlem  25772  iblcnlem1  25838  iblre  25844  iblcn  25849  logfaclbnd  27274  ons2ind  28356  axcontlem4  29125  axcontlem7  29128  ocsh  31443  pjhthmo  31462  5oalem6  31819  cvnbtwn4  32449  superpos  32514  cdj3i  32601  13an22anass  32622  smatrcl  34054  ordtrest2NEWlem  34180  cusgr3cyclex  35447  lineext  36387  outsideoftr  36440  hilbert1.2  36466  lineintmo  36468  neibastop1  36680  bj-inrab  37373  isbasisrelowllem1  37810  isbasisrelowllem2  37811  ptrest  38079  poimirlem26  38106  ismblfin  38121  unirep  38174  inixp  38188  ablo4pnp  38340  keridl  38492  ispridlc  38530  anan  38695  disjecxrn  38872  coss1cnvres  38967  br1cosscnvxrn  39024  dfeldisj3  39271  antisymrelres  39326  prtlem70  39442  lcvbr3  39608  cvrnbtwn4  39864  linepsubN  40337  pmapsub  40353  pmapjoin  40437  ltrnu  40706  diblsmopel  41756  pell1234qrmulcl  43393  ifpan23  43997  ifpidg  44028  ifpbibib  44047  uneqsn  44562  isthincd2  50019