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  4451  disjiun  5060  inxp  5774  xp11  6126  dfpo2  6247  fununi  6560  fun  6689  resoprab2  7475  sorpsscmpl  7677  xporderlem  8067  poxp  8068  poseq  8098  fprlem1  8240  frrlem15  9672  dfac5lem1  10036  zorn2lem6  10414  cju  12146  ixxin  13306  elfzo2  13607  xpcogend  14927  summo  15670  prodmo  15892  dfiso2  17730  issubmd  18765  gsumval3eu  19870  dvdsrtr  20339  isirred2  20392  domnmuln0  20681  isdomn3  20687  abvn0b  20808  lspsolvlem  21135  unocv  21655  pf1ind  22341  ordtrest2lem  23186  lmmo  23363  ptbasin  23560  txbasval  23589  txcnp  23603  txlm  23631  tx1stc  23633  tx2ndc  23634  isfild  23841  txflf  23989  isclmp  25082  mbfi1flimlem  25707  iblcnlem1  25773  iblre  25779  iblcn  25784  logfaclbnd  27203  ons2ind  28285  axcontlem4  29054  axcontlem7  29057  ocsh  31372  pjhthmo  31391  5oalem6  31748  cvnbtwn4  32378  superpos  32443  cdj3i  32530  13an22anass  32551  smatrcl  33980  ordtrest2NEWlem  34106  cusgr3cyclex  35364  lineext  36304  outsideoftr  36357  hilbert1.2  36383  lineintmo  36385  neibastop1  36587  bj-inrab  37280  isbasisrelowllem1  37717  isbasisrelowllem2  37718  ptrest  37986  poimirlem26  38013  ismblfin  38028  unirep  38081  inixp  38095  ablo4pnp  38247  keridl  38399  ispridlc  38437  anan  38602  disjecxrn  38779  coss1cnvres  38874  br1cosscnvxrn  38931  dfeldisj3  39178  antisymrelres  39233  prtlem70  39349  lcvbr3  39515  cvrnbtwn4  39771  linepsubN  40244  pmapsub  40260  pmapjoin  40344  ltrnu  40613  diblsmopel  41663  pell1234qrmulcl  43300  ifpan23  43904  ifpidg  43935  ifpbibib  43954  uneqsn  44469  isthincd2  49927