Theorem an4 865

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 838	. . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃)))
2	1	anbi2i 730	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃))))
3		anass 681	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
4		anass 681	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃))))
5	2, 3, 4	3bitr4i 292	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))

Syntax hints:   ↔ wb 196   ∧ wa 384

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 386

This theorem is referenced by:  an42  866  an4s  869  anandi  871  anandir  872  an6  1408  an33rean  1446  reean  3106  reu2  3394  rmo4  3399  rmo3  3528  disjiun  4640  inxp  5254  xp11  5569  fununi  5964  fun  6066  resoprab2  6757  sorpsscmpl  6948  xporderlem  7288  poxp  7289  dfac5lem1  8946  zorn2lem6  9323  cju  11016  ixxin  12192  elfzo2  12473  xpcogend  13713  summo  14448  prodmo  14666  dfiso2  16432  issubmd  17349  gsumval3eu  18305  dvdsrtr  18652  isirred2  18701  lspsolvlem  19142  domnmuln0  19298  abvn0b  19302  pf1ind  19719  unocv  20024  ordtrest2lem  21007  lmmo  21184  ptbasin  21380  txbasval  21409  txcnp  21423  txlm  21451  tx1stc  21453  tx2ndc  21454  isfild  21662  txflf  21810  isclmp  22897  mbfi1flimlem  23489  iblcnlem1  23554  iblre  23560  iblcn  23565  logfaclbnd  24947  axcontlem4  25847  axcontlem7  25850  ocsh  28142  pjhthmo  28161  5oalem6  28518  cvnbtwn4  29148  superpos  29213  cdj3i  29300  rmo3f  29335  rmo4fOLD  29336  smatrcl  29862  ordtrest2NEWlem  29968  dfpo2  31645  poseq  31750  lineext  32183  outsideoftr  32236  hilbert1.2  32262  lineintmo  32264  neibastop1  32354  bj-inrab  32923  isbasisrelowllem1  33203  isbasisrelowllem2  33204  ptrest  33408  poimirlem26  33435  ismblfin  33450  unirep  33507  inixp  33523  ablo4pnp  33679  keridl  33831  ispridlc  33869  anan  33999  prtlem70  34141  lcvbr3  34310  cvrnbtwn4  34566  linepsubN  35038  pmapsub  35054  pmapjoin  35138  ltrnu  35407  diblsmopel  36460  pell1234qrmulcl  37419  isdomn3  37782  ifpan23  37804  ifpidg  37836  ifpbibib  37855  uneqsn  38321  2reu1  41186  2reu4a  41189