Theorem an4 900

Description: Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)

Assertion

Ref	Expression
an4	⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Proof of Theorem an4

Step	Hyp	Ref	Expression
1		an12 873	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
2	1	anbi2i 732	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃))))
3		anass 684	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
4		anass 684	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃))))
5	2, 3, 4	3bitr4i 292	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Syntax hints:   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  an42  901  an4s  904  anandi  906  anandir  907  an6  1555  an33rean  1593  reean  3242  reu2  3533  rmo4  3538  rmo3  3667  disjiun  4790  inxp  5408  xp11  5725  fununi  6123  fun  6225  resoprab2  6920  sorpsscmpl  7111  xporderlem  7454  poxp  7455  dfac5lem1  9134  zorn2lem6  9513  cju  11206  ixxin  12383  elfzo2  12665  xpcogend  13912  summo  14645  prodmo  14863  dfiso2  16631  issubmd  17548  gsumval3eu  18503  dvdsrtr  18850  isirred2  18899  lspsolvlem  19342  domnmuln0  19498  abvn0b  19502  pf1ind  19919  unocv  20224  ordtrest2lem  21207  lmmo  21384  ptbasin  21580  txbasval  21609  txcnp  21623  txlm  21651  tx1stc  21653  tx2ndc  21654  isfild  21861  txflf  22009  isclmp  23095  mbfi1flimlem  23686  iblcnlem1  23751  iblre  23757  iblcn  23762  logfaclbnd  25144  axcontlem4  26044  axcontlem7  26047  ocsh  28449  pjhthmo  28468  5oalem6  28825  cvnbtwn4  29455  superpos  29520  cdj3i  29607  rmo3f  29641  rmo4fOLD  29642  smatrcl  30169  ordtrest2NEWlem  30275  dfpo2  31950  poseq  32057  lineext  32487  outsideoftr  32540  hilbert1.2  32566  lineintmo  32568  neibastop1  32658  bj-inrab  33227  isbasisrelowllem1  33512  isbasisrelowllem2  33513  ptrest  33719  poimirlem26  33746  ismblfin  33761  unirep  33818  inixp  33834  ablo4pnp  33990  keridl  34142  ispridlc  34180  anan  34323  br1cosscnvxrn  34545  prtlem70  34643  lcvbr3  34811  cvrnbtwn4  35067  linepsubN  35539  pmapsub  35555  pmapjoin  35639  ltrnu  35908  diblsmopel  36960  pell1234qrmulcl  37919  isdomn3  38282  ifpan23  38304  ifpidg  38336  ifpbibib  38355  uneqsn  38821  2reu1  41690  2reu4a  41693