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  3200  reu2  3687  rmo4  3692  rmo3f  3696  rmo3  3843  2reu1  3851  2reu4lem  4475  disjiun  5083  inxp  5778  inxpOLD  5779  xp11  6128  dfpo2  6248  fununi  6561  fun  6690  resoprab2  7472  sorpsscmpl  7674  xporderlem  8067  poxp  8068  poseq  8098  fprlem1  8240  frrlem15  9672  dfac5lem1  10036  zorn2lem6  10414  cju  12143  ixxin  13284  elfzo2  13584  xpcogend  14900  summo  15643  prodmo  15862  dfiso2  17698  issubmd  18699  gsumval3eu  19802  dvdsrtr  20272  isirred2  20325  domnmuln0  20613  isdomn3  20619  abvn0b  20740  lspsolvlem  21068  unocv  21606  pf1ind  22259  ordtrest2lem  23107  lmmo  23284  ptbasin  23481  txbasval  23510  txcnp  23524  txlm  23552  tx1stc  23554  tx2ndc  23555  isfild  23762  txflf  23910  isclmp  25014  mbfi1flimlem  25640  iblcnlem1  25706  iblre  25712  iblcn  25717  logfaclbnd  27150  axcontlem4  28931  axcontlem7  28934  ocsh  31246  pjhthmo  31265  5oalem6  31622  cvnbtwn4  32252  superpos  32317  cdj3i  32404  13an22anass  32427  smatrcl  33782  ordtrest2NEWlem  33908  cusgr3cyclex  35128  lineext  36069  outsideoftr  36122  hilbert1.2  36148  lineintmo  36150  neibastop1  36352  bj-inrab  36920  isbasisrelowllem1  37348  isbasisrelowllem2  37349  ptrest  37618  poimirlem26  37645  ismblfin  37660  unirep  37713  inixp  37727  ablo4pnp  37879  keridl  38031  ispridlc  38069  anan  38222  disjecxrn  38380  coss1cnvres  38413  br1cosscnvxrn  38470  dfeldisj3  38716  antisymrelres  38760  prtlem70  38855  lcvbr3  39021  cvrnbtwn4  39277  linepsubN  39751  pmapsub  39767  pmapjoin  39851  ltrnu  40120  diblsmopel  41170  pell1234qrmulcl  42848  ifpan23  43453  ifpidg  43484  ifpbibib  43503  uneqsn  44018  isthincd2  49442