Theorem an4 654

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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 399

This theorem is referenced by:  an42  655  an4s  658  anandi  674  anandir  675  an6  1441  an33reanOLD  1480  reeanlem  3368  reu2  3719  rmo4  3724  rmo3f  3728  rmo3  3875  rmo3OLD  3876  2reu1  3884  2reu4lem  4468  disjiun  5056  inxp  5706  xp11  6035  fununi  6432  fun  6543  resoprab2  7274  sorpsscmpl  7463  xporderlem  7824  poxp  7825  dfac5lem1  9552  zorn2lem6  9926  cju  11637  ixxin  12758  elfzo2  13044  xpcogend  14337  summo  15077  prodmo  15293  dfiso2  17045  issubmd  17974  gsumval3eu  19027  dvdsrtr  19405  isirred2  19454  lspsolvlem  19917  domnmuln0  20074  abvn0b  20078  pf1ind  20521  unocv  20827  ordtrest2lem  21814  lmmo  21991  ptbasin  22188  txbasval  22217  txcnp  22231  txlm  22259  tx1stc  22261  tx2ndc  22262  isfild  22469  txflf  22617  isclmp  23704  mbfi1flimlem  24326  iblcnlem1  24391  iblre  24397  iblcn  24402  logfaclbnd  25801  axcontlem4  26756  axcontlem7  26759  ocsh  29063  pjhthmo  29082  5oalem6  29439  cvnbtwn4  30069  superpos  30134  cdj3i  30221  smatrcl  31065  ordtrest2NEWlem  31169  cusgr3cyclex  32387  dfpo2  32995  poseq  33099  fprlem1  33141  frrlem15  33146  lineext  33541  outsideoftr  33594  hilbert1.2  33620  lineintmo  33622  neibastop1  33711  bj-inrab  34249  isbasisrelowllem1  34640  isbasisrelowllem2  34641  ptrest  34895  poimirlem26  34922  ismblfin  34937  unirep  34992  inixp  35007  ablo4pnp  35162  keridl  35314  ispridlc  35352  anan  35503  br1cosscnvxrn  35718  dfeldisj3  35956  prtlem70  35997  lcvbr3  36163  cvrnbtwn4  36419  linepsubN  36892  pmapsub  36908  pmapjoin  36992  ltrnu  37261  diblsmopel  38311  pell1234qrmulcl  39458  isdomn3  39810  ifpan23  39831  ifpidg  39863  ifpbibib  39882  uneqsn  40379