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  3206  reu2  3693  rmo4  3698  rmo3f  3702  rmo3  3849  2reu1  3857  2reu4lem  4481  disjiun  5090  inxp  5785  inxpOLD  5786  xp11  6136  dfpo2  6257  fununi  6575  fun  6704  resoprab2  7488  sorpsscmpl  7690  xporderlem  8083  poxp  8084  poseq  8114  fprlem1  8256  frrlem15  9686  dfac5lem1  10052  zorn2lem6  10430  cju  12158  ixxin  13299  elfzo2  13599  xpcogend  14916  summo  15659  prodmo  15878  dfiso2  17710  issubmd  18709  gsumval3eu  19810  dvdsrtr  20253  isirred2  20306  domnmuln0  20594  isdomn3  20600  abvn0b  20721  lspsolvlem  21028  unocv  21565  pf1ind  22218  ordtrest2lem  23066  lmmo  23243  ptbasin  23440  txbasval  23469  txcnp  23483  txlm  23511  tx1stc  23513  tx2ndc  23514  isfild  23721  txflf  23869  isclmp  24973  mbfi1flimlem  25599  iblcnlem1  25665  iblre  25671  iblcn  25676  logfaclbnd  27109  axcontlem4  28870  axcontlem7  28873  ocsh  31185  pjhthmo  31204  5oalem6  31561  cvnbtwn4  32191  superpos  32256  cdj3i  32343  13an22anass  32366  smatrcl  33759  ordtrest2NEWlem  33885  cusgr3cyclex  35096  lineext  36037  outsideoftr  36090  hilbert1.2  36116  lineintmo  36118  neibastop1  36320  bj-inrab  36888  isbasisrelowllem1  37316  isbasisrelowllem2  37317  ptrest  37586  poimirlem26  37613  ismblfin  37628  unirep  37681  inixp  37695  ablo4pnp  37847  keridl  37999  ispridlc  38037  anan  38190  disjecxrn  38348  coss1cnvres  38381  br1cosscnvxrn  38438  dfeldisj3  38684  antisymrelres  38728  prtlem70  38823  lcvbr3  38989  cvrnbtwn4  39245  linepsubN  39719  pmapsub  39735  pmapjoin  39819  ltrnu  40088  diblsmopel  41138  pell1234qrmulcl  42816  ifpan23  43422  ifpidg  43453  ifpbibib  43472  uneqsn  43987  isthincd2  49399