Theorem an4 655

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 472	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
2		an12 644	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
3	2	bianass 641	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))
4	1, 3	bitri 278	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Syntax hints:   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  an42  656  an4s  659  anandi  675  anandir  676  an6  1442  an33reanOLD  1481  reeanlem  3318  reu2  3664  rmo4  3669  rmo3f  3673  rmo3  3818  2reu1  3826  2reu4lem  4423  disjiun  5017  inxp  5667  xp11  5999  fununi  6399  fun  6514  resoprab2  7250  sorpsscmpl  7440  xporderlem  7804  poxp  7805  dfac5lem1  9534  zorn2lem6  9912  cju  11621  ixxin  12743  elfzo2  13036  xpcogend  14325  summo  15066  prodmo  15282  dfiso2  17034  issubmd  17963  gsumval3eu  19017  dvdsrtr  19398  isirred2  19447  lspsolvlem  19907  domnmuln0  20064  abvn0b  20068  unocv  20369  pf1ind  20979  ordtrest2lem  21808  lmmo  21985  ptbasin  22182  txbasval  22211  txcnp  22225  txlm  22253  tx1stc  22255  tx2ndc  22256  isfild  22463  txflf  22611  isclmp  23702  mbfi1flimlem  24326  iblcnlem1  24391  iblre  24397  iblcn  24402  logfaclbnd  25806  axcontlem4  26761  axcontlem7  26764  ocsh  29066  pjhthmo  29085  5oalem6  29442  cvnbtwn4  30072  superpos  30137  cdj3i  30224  smatrcl  31149  ordtrest2NEWlem  31275  cusgr3cyclex  32496  dfpo2  33104  poseq  33208  fprlem1  33250  frrlem15  33255  lineext  33650  outsideoftr  33703  hilbert1.2  33729  lineintmo  33731  neibastop1  33820  bj-inrab  34369  isbasisrelowllem1  34772  isbasisrelowllem2  34773  ptrest  35056  poimirlem26  35083  ismblfin  35098  unirep  35151  inixp  35166  ablo4pnp  35318  keridl  35470  ispridlc  35508  anan  35659  br1cosscnvxrn  35874  dfeldisj3  36112  prtlem70  36153  lcvbr3  36319  cvrnbtwn4  36575  linepsubN  37048  pmapsub  37064  pmapjoin  37148  ltrnu  37417  diblsmopel  38467  pell1234qrmulcl  39796  isdomn3  40148  ifpan23  40168  ifpidg  40199  ifpbibib  40218  uneqsn  40726