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  3204  reu2  3680  rmo4  3685  rmo3f  3689  rmo3  3836  2reu1  3844  2reu4lem  4473  disjiun  5083  inxp  5777  inxpOLD  5778  xp11  6130  dfpo2  6251  fununi  6564  fun  6693  resoprab2  7474  sorpsscmpl  7676  xporderlem  8066  poxp  8067  poseq  8097  fprlem1  8239  frrlem15  9661  dfac5lem1  10025  zorn2lem6  10403  cju  12132  ixxin  13269  elfzo2  13569  xpcogend  14888  summo  15631  prodmo  15850  dfiso2  17687  issubmd  18722  gsumval3eu  19824  dvdsrtr  20295  isirred2  20348  domnmuln0  20633  isdomn3  20639  abvn0b  20760  lspsolvlem  21088  unocv  21626  pf1ind  22290  ordtrest2lem  23138  lmmo  23315  ptbasin  23512  txbasval  23541  txcnp  23555  txlm  23583  tx1stc  23585  tx2ndc  23586  isfild  23793  txflf  23941  isclmp  25044  mbfi1flimlem  25670  iblcnlem1  25736  iblre  25742  iblcn  25747  logfaclbnd  27180  axcontlem4  28966  axcontlem7  28969  ocsh  31284  pjhthmo  31303  5oalem6  31660  cvnbtwn4  32290  superpos  32355  cdj3i  32442  13an22anass  32464  smatrcl  33881  ordtrest2NEWlem  34007  cusgr3cyclex  35252  lineext  36192  outsideoftr  36245  hilbert1.2  36271  lineintmo  36273  neibastop1  36475  bj-inrab  37044  isbasisrelowllem1  37472  isbasisrelowllem2  37473  ptrest  37732  poimirlem26  37759  ismblfin  37774  unirep  37827  inixp  37841  ablo4pnp  37993  keridl  38145  ispridlc  38183  anan  38343  disjecxrn  38509  coss1cnvres  38592  br1cosscnvxrn  38649  dfeldisj3  38890  antisymrelres  38934  prtlem70  39029  lcvbr3  39195  cvrnbtwn4  39451  linepsubN  39924  pmapsub  39940  pmapjoin  40024  ltrnu  40293  diblsmopel  41343  pell1234qrmulcl  43012  ifpan23  43617  ifpidg  43648  ifpbibib  43667  uneqsn  44182  isthincd2  49598