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  3228  reu2  3731  rmo4  3736  rmo3f  3740  rmo3  3889  2reu1  3897  2reu4lem  4522  disjiun  5131  inxp  5842  inxpOLD  5843  xp11  6195  dfpo2  6316  fununi  6641  fun  6770  resoprab2  7552  sorpsscmpl  7754  xporderlem  8152  poxp  8153  poseq  8183  fprlem1  8325  frrlem15  9797  dfac5lem1  10163  zorn2lem6  10541  cju  12262  ixxin  13404  elfzo2  13702  xpcogend  15013  summo  15753  prodmo  15972  dfiso2  17816  issubmd  18819  gsumval3eu  19922  dvdsrtr  20368  isirred2  20421  domnmuln0  20709  isdomn3  20715  abvn0b  20837  lspsolvlem  21144  unocv  21698  pf1ind  22359  ordtrest2lem  23211  lmmo  23388  ptbasin  23585  txbasval  23614  txcnp  23628  txlm  23656  tx1stc  23658  tx2ndc  23659  isfild  23866  txflf  24014  isclmp  25130  mbfi1flimlem  25757  iblcnlem1  25823  iblre  25829  iblcn  25834  logfaclbnd  27266  axcontlem4  28982  axcontlem7  28985  ocsh  31302  pjhthmo  31321  5oalem6  31678  cvnbtwn4  32308  superpos  32373  cdj3i  32460  13an22anass  32483  smatrcl  33795  ordtrest2NEWlem  33921  cusgr3cyclex  35141  lineext  36077  outsideoftr  36130  hilbert1.2  36156  lineintmo  36158  neibastop1  36360  bj-inrab  36928  isbasisrelowllem1  37356  isbasisrelowllem2  37357  ptrest  37626  poimirlem26  37653  ismblfin  37668  unirep  37721  inixp  37735  ablo4pnp  37887  keridl  38039  ispridlc  38077  anan  38230  disjecxrn  38390  coss1cnvres  38418  br1cosscnvxrn  38475  dfeldisj3  38720  antisymrelres  38764  prtlem70  38858  lcvbr3  39024  cvrnbtwn4  39280  linepsubN  39754  pmapsub  39770  pmapjoin  39854  ltrnu  40123  diblsmopel  41173  pell1234qrmulcl  42866  ifpan23  43473  ifpidg  43504  ifpbibib  43523  uneqsn  44038  isthincd2  49086