Theorem an4 662

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

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

This theorem is referenced by:  an42  663  an4s  666  anandi  682  anandir  683  an6  1453  reeanlem  3210  reu2  3666  rmo4  3671  rmo3f  3675  rmo3  3821  2reu1  3829  2reu4lem  4452  disjiun  5061  inxp  5775  xp11  6127  dfpo2  6248  fununi  6561  fun  6690  resoprab2  7476  sorpsscmpl  7678  xporderlem  8068  poxp  8069  poseq  8099  fprlem1  8241  frrlem15  9673  dfac5lem1  10037  zorn2lem6  10415  cju  12147  ixxin  13307  elfzo2  13608  xpcogend  14928  summo  15671  prodmo  15893  dfiso2  17731  issubmd  18766  gsumval3eu  19871  dvdsrtr  20340  isirred2  20393  domnmuln0  20682  isdomn3  20688  abvn0b  20809  lspsolvlem  21136  unocv  21656  pf1ind  22342  ordtrest2lem  23187  lmmo  23364  ptbasin  23561  txbasval  23590  txcnp  23604  txlm  23632  tx1stc  23634  tx2ndc  23635  isfild  23842  txflf  23990  isclmp  25083  mbfi1flimlem  25708  iblcnlem1  25774  iblre  25780  iblcn  25785  logfaclbnd  27204  ons2ind  28286  axcontlem4  29055  axcontlem7  29058  ocsh  31373  pjhthmo  31392  5oalem6  31749  cvnbtwn4  32379  superpos  32444  cdj3i  32531  13an22anass  32552  smatrcl  33989  ordtrest2NEWlem  34115  cusgr3cyclex  35373  lineext  36313  outsideoftr  36366  hilbert1.2  36392  lineintmo  36394  neibastop1  36596  bj-inrab  37289  isbasisrelowllem1  37726  isbasisrelowllem2  37727  ptrest  37995  poimirlem26  38022  ismblfin  38037  unirep  38090  inixp  38104  ablo4pnp  38256  keridl  38408  ispridlc  38446  anan  38611  disjecxrn  38788  coss1cnvres  38883  br1cosscnvxrn  38940  dfeldisj3  39187  antisymrelres  39242  prtlem70  39358  lcvbr3  39524  cvrnbtwn4  39780  linepsubN  40253  pmapsub  40269  pmapjoin  40353  ltrnu  40622  diblsmopel  41672  pell1234qrmulcl  43309  ifpan23  43913  ifpidg  43944  ifpbibib  43963  uneqsn  44478  isthincd2  49935